Code

error-less io#6

Code

Closed

Kha wants to merge 11 commits intomasterleanprover/lean4:masterfrom eioleanprover/lean4:eioCopy head branch name to clipboard

+712-675

Commits

Commits on Aug 17, 2018

• feat(library/noncomputable): mark all VM builtins as computable

  Kha

  committed
  3088c66

  Copy full SHA for 3088c66

• feat(library/noncomputable): sorts are computable

  Show description for f6ba637
  Kha

  committed
  f6ba637

  Copy full SHA for f6ba637

• refactor(library/vm/vm_io,library/system/io): remove io classes, make errors explicit

  Kha

  committed
  e7e98f1

  Copy full SHA for e7e98f1

• refactor(library/system/io): move into init

  Kha

  committed
  4030a2d

  Copy full SHA for 4030a2d

• feat(library/init/io): introduce has_eval class to customize #eval output

  Kha

  committed
  5555d3f

  Copy full SHA for 5555d3f

• fix(library/{vm/vm_io,init/io}): fix bugs and tests

  Kha

  committed
  afc4c5e

  Copy full SHA for afc4c5e

• feat(library/init/{io,control/except}): use lift_t to automatically upcast io and other errors

  Kha

  committed
  7cf2452

  Copy full SHA for 7cf2452

• refactor(library/init/io): replace ioe with eio

  Show description for 7acc674
  Kha

  committed
  7acc674

  Copy full SHA for 7acc674

• fix(library/vm/vm_io): move all primitives into io

  Show description for 1ba3c3c
  Kha

  committed
  1ba3c3c

  Copy full SHA for 1ba3c3c

• feat(library/init/control/coroutine_io): coroutine_io

  Kha

  committed
  7bd57c9

  Copy full SHA for 7bd57c9

• chore(library/init/io): rename io.print_ln to io.println

  Kha

  committed
  8e4aed5

  Copy full SHA for 8e4aed5