Code

Lean boot#10

Code

Closed

Kha wants to merge 7 commits intomasterleanprover/lean4:masterfrom lean_bootleanprover/lean4:lean_bootCopy head branch name to clipboard

+185-332

Commits

Commits on Feb 14, 2019

• feat(frontends/lean/vm_elaborator): port to new runtime

  Kha

  committed
  3221f3c

  Copy full SHA for 3221f3c

• feat(shell/lean): --new-frontend

  Show description for 1702911
  Kha

  committed
  1702911

  Copy full SHA for 1702911

• fix(library/messages): message_severity is unboxed

  Kha

  committed
  48835ee

  Copy full SHA for 48835ee

• feat(library/init/lean/{parser/term,elaborator}): support @& borrowed annotations

  Kha

  committed
  5b8f5cb

  Copy full SHA for 5b8f5cb

• feat(library/init/lean/elaborator): to_pexpr: support string literals

  Kha

  committed
  ec7687f

  Copy full SHA for ec7687f

• chore(frontends/lean/vm_elaborator): ignore [extern] for now

  Kha

  committed
  47170ea

  Copy full SHA for 47170ea

• chore(library/compiler/extern_attribute): style

  Kha

  committed
  2757069

  Copy full SHA for 2757069