feat(frontends/lean, library/init/lean): opaque constants

@kha I have added support for opaque constants to the old C++ frontend,
and made sure the new frontend can still parse `library/init/core.lean`.
The kernel should enforce that opaque constants are really opaque, and
the following example should fail
```
constant x : nat := 0
theorem foo : x = 0 := rfl
```
If it doesn't, it is a bug.

Here are some remaining issues:
1- `environment.mk_empty` is currently an axiom because we cannot create
an inhabitant of an opaque type. A possible solution is to use
`option environment` instead of `environment`.

2- There is no support for opaque constants in the new
frontend. However, I modified it to handle axioms, and fixed the literal
values with decl_cmd_kind. I tried to mark some of my changes with
comments, but it is probably much easier for you to just check the
commit change list.

3- I did not add any support for automatically constructing `e`
at `constant x : t := e`. I think we can do this later
after we replace the old frontend with the new one. BTW, it took only a
few minutes to provide the inhabitants manually.

lean4-mode/lean4-syntax.el

@@ -9,9 +9,9 @@
 
 (defconst lean4-keywords1
   '("import" "prelude" "protected" "private" "noncomputable" "definition" "unsafe" "renaming"
-    "hiding" "exposing" "parameter" "parameters" "begin" "constant" "constants"
+    "hiding" "exposing" "parameter" "parameters" "begin" "constant"
     "lemma" "variable" "variables" "theorem" "example" "abbreviation" "abbrev"
-    "open" "export" "axiom" "axioms" "inductive" "coinductive" "with" "without"
+    "open" "export" "axiom" "inductive" "coinductive" "with" "without"
     "structure" "universe" "universes" "hide"
     "precedence" "reserve" "declare_trace" "add_key_equivalence"
     "match" "infix" "infixl" "infixr" "notation" "postfix" "prefix" "instance"
@@ -142,7 +142,7 @@
       (1 'font-lock-function-name-face))
      ;; declarations
      (,(rx word-start
-           (group (or "inductive" (group "class" (zero-or-more whitespace) "inductive") "instance" "structure" "class" "theorem" "axiom" "axioms" "lemma" "definition" "def" "constant"))
+           (group (or "inductive" (group "class" (zero-or-more whitespace) "inductive") "instance" "structure" "class" "theorem" "axiom" "lemma" "definition" "def" "constant"))
            word-end (zero-or-more whitespace)
            (group (zero-or-more "{" (zero-or-more (not (any "}"))) "}" (zero-or-more whitespace)))
            (zero-or-more whitespace)

library/init/core.lean

@@ -337,7 +337,7 @@ inductive nat
 /- Auxiliary axiom used to implement `sorry`.
    TODO: add this theorem on-demand. That is,
    we should only add it if after the first error. -/
-constant sorry_ax (α : Sort u) (synthetic := tt) : α
+unsafe axiom sorry_ax (α : Sort u) (synthetic := tt) : α
 
 /- Declare builtin and reserved notation -/
 
@@ -1724,7 +1724,7 @@ end setoid
 
 /- Propositional extensionality -/
 
-constant propext {a b : Prop} : (a ↔ b) → a = b
+axiom propext {a b : Prop} : (a ↔ b) → a = b
 
 /- Additional congruence theorems. -/
 
@@ -1766,7 +1766,7 @@ theorem iff_subst {a b : Prop} {p : Prop → Prop} (h₁ : a ↔ b) (h₂ : p a)
 eq.subst (propext h₁) h₂
 
 namespace quot
-constant sound : Π {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → quot.mk r a = quot.mk r b
+axiom sound : Π {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → quot.mk r a = quot.mk r b
 
 attribute [elab_as_eliminator] lift ind
 

library/init/data/char/basic.lean

@@ -42,8 +42,10 @@ uint32.dec_lt _ _
 instance dec_le (a b : char) : decidable (a ≤ b) :=
 uint32.dec_le _ _
 
+axiom is_valid_char_0 : is_valid_char 0
+
 @[noinline, pattern] def of_nat (n : nat) : char :=
-if h : is_valid_char (uint32.of_nat n) then {val := uint32.of_nat n, valid := h} else {val := 0, valid := sorry}
+if h : is_valid_char (uint32.of_nat n) then {val := uint32.of_nat n, valid := h} else {val := 0, valid := is_valid_char_0}
 
 @[inline] def to_nat (c : char) : nat :=
 c.val.to_nat

library/init/io.lean

@@ -8,19 +8,20 @@ import init.control.state init.control.except init.data.string.basic init.fix
 
 /-- Like https://hackage.haskell.org/package/ghc-prim-0.5.2.0/docs/GHC-Prim.html#t:RealWorld.
     Makes sure we never reorder `io` operations. -/
-constant io.real_world : Type
+constant io.real_world : Type := unit
+
 -- TODO: make opaque
 @[irreducible, derive monad]
 def io : Type → Type := state io.real_world
 
 @[extern "lean_io_unsafe"]
-constant unsafe_io {α : Type} [inhabited α] (fn : io α) : α
+constant unsafe_io {α : Type} [inhabited α] (fn : io α) : α := default α
 
 @[extern 4 "lean_io_timeit"]
-constant timeit {α : Type} (msg : @& string) (fn : io α) : io α
+constant timeit {α : Type} (msg : @& string) (fn : io α) : io α := fn
 
 @[extern 4 "lean_io_allocprof"]
-constant allocprof {α : Type} (msg : @& string) (fn : io α) : io α
+constant allocprof {α : Type} (msg : @& string) (fn : io α) : io α := fn
 
 abbrev monad_io (m : Type → Type) := has_monad_lift_t io m
 
@@ -56,7 +57,7 @@ end
 
 inductive fs.mode
 | read | write | read_write | append
-constant fs.handle : Type
+constant fs.handle : Type := unit
 
 namespace prim
 open fs
@@ -85,23 +86,30 @@ iterate a $ λ r, do
   | except.ok (sum.inr r) := pure (sum.inr (except.ok r))
   | except.error e        := pure (sum.inr (except.error e))
 
+
+section
+local attribute [reducible] io
+def eio_inh {α : Type} : eio α :=
+λ s, (except.error (default io.error), s)
+end
+
 @[extern 2 "lean_io_prim_put_str"]
-constant put_str (s: @& string) : eio unit
+constant put_str (s: @& string) : eio unit := eio_inh
 @[extern 1 "lean_io_prim_get_line"]
-constant get_line : eio string
+constant get_line : eio string := eio_inh
 @[extern 4 "lean_io_prim_handle_mk"]
-constant handle.mk (s : @& string) (m : mode) (bin : bool := ff) : eio handle
+constant handle.mk (s : @& string) (m : mode) (bin : bool := ff) : eio handle := eio_inh
 @[extern 2 "lean_io_prim_handle_is_eof"]
-constant handle.is_eof (h : @& handle) : eio bool
+constant handle.is_eof (h : @& handle) : eio bool := eio_inh
 @[extern 2 "lean_io_prim_handle_flush"]
-constant handle.flush (h : @& handle) : eio unit
+constant handle.flush (h : @& handle) : eio unit := eio_inh
 @[extern 2 "lean_io_prim_handle_close"]
-constant handle.close (h : @& handle) : eio unit
+constant handle.close (h : @& handle) : eio unit := eio_inh
 -- TODO: replace `string` with byte buffer
 -- constant handle.read : handle → nat → eio string
 -- constant handle.write : handle → string → eio unit
 @[extern 2 "lean_io_prim_handle_get_line"]
-constant handle.get_line (h : @& handle) : eio string
+constant handle.get_line (h : @& handle) : eio string := eio_inh
 
 @[inline] def lift_eio {m : Type → Type} {ε α : Type} [monad_io m] [monad_except ε m] [has_lift_t io.error ε] [monad m]
   (x : eio α) : m α :=

library/init/lean/elaborator.lean

@@ -13,14 +13,16 @@ import init.lean.options
 
 namespace lean
 -- TODO(Sebastian): should probably be meta together with the whole elaborator
-constant environment : Type
+constant environment : Type := unit
+
 @[extern "lean_environment_mk_empty"]
-constant environment.mk_empty : unit → environment
+axiom environment.mk_empty : unit → environment
+
 @[extern "lean_environment_contains"]
-constant environment.contains : (@& environment) → (@& name) → bool
+constant environment.contains (env : @& environment) (n : @& name) : bool := ff
 -- deprecated constructor
 @[extern "lean_expr_local"]
-constant expr.local : name → name → expr → binder_info → expr
+constant expr.local (n : name) (pp : name) (ty : expr) (bi : binder_info) : expr := default expr
 
 namespace elaborator
 -- TODO(Sebastian): move
@@ -46,8 +48,7 @@ structure old_elaborator_state :=
 (ns : name)
 
 @[extern "lean_elaborator_elaborate_command"]
-constant elaborate_command (filename : @& string) : expr → (@& old_elaborator_state) →
-  option old_elaborator_state × message_log
+constant elaborate_command (filename : @& string) (e : expr) (s : @& old_elaborator_state) : option old_elaborator_state × message_log := (none, ⟨[]⟩)
 
 open parser
 open parser.combinators
@@ -460,8 +461,8 @@ def declaration.elaborate : elaborator :=
 λ stx, locally $ do
   let decl := view «declaration» stx,
   match decl.inner with
-  | declaration.inner.view.constant c@{sig := {params := bracketed_binders.view.simple [], type := type}, ..} := do
-    let mdata := kvmap.set_name {} `command `constant,
+  | declaration.inner.view.«axiom» c@{sig := {params := bracketed_binders.view.simple [], type := type}, ..} := do
+    let mdata := kvmap.set_name {} `command `«axiom», -- CommentTo(Kha): It was `constant` here
     mods ← decl_modifiers_to_pexpr decl.modifiers,
     let id := ident_univ_params_to_pexpr c.name,
     type ← to_pexpr type.type,
@@ -470,8 +471,8 @@ def declaration.elaborate : elaborator :=
       let kind := match dl.kind with
       | def_like.kind.view.theorem _ := 0
       | def_like.kind.view.def _ := 1
-      | def_like.kind.view.abbreviation _ := 5
-      | def_like.kind.view.«abbrev» _ := 5,
+      | def_like.kind.view.abbreviation _ := 6
+      | def_like.kind.view.«abbrev» _ := 6,
       elab_def_like stx decl.modifiers dl kind
 
   -- these are almost macros for `def`, except the elaborator handles them specially at a few places
@@ -481,13 +482,13 @@ def declaration.elaborate : elaborator :=
       kind := def_like.kind.view.def,
       name := {id := name.anonymous},
       sig := {..ex.sig},
-      ..ex} 2
+      ..ex} 3
   | declaration.inner.view.instance i :=
     elab_def_like stx decl.modifiers {
       kind := def_like.kind.view.def,
       name := i.name.get_or_else {id := name.anonymous},
       sig := {..i.sig},
-      ..i} 3
+      ..i} 4
 
   | declaration.inner.view.inductive ind@{«class» := none, sig := {params := bracketed_binders.view.simple bbs}, ..} := do
     let mdata := kvmap.set_name {} `command `inductives,

library/init/lean/expander.lean

@@ -372,15 +372,15 @@ def let.transform : transformer :=
       equations := [{item := {lhs := [llp], rhs := v.body}}]}
 
 -- move parameters into type
-def constant.transform : transformer :=
+def axiom.transform : transformer :=
 λ stx, do
-  let v := view «constant» stx,
+  let v := view «axiom» stx,
   match v with
   | {sig := {params := bracketed_binders.view.extended bindrs, type := type}, ..} := do
     let bindrs := binders.view.extended {
       leading_ids := [],
       remainder := binders_remainder.view.mixed $ bindrs.map mixed_binder.view.bracketed},
-    pure $ review «constant» {v with sig := {
+    pure $ review «axiom» {v with sig := {
       params := bracketed_binders.view.simple [],
       type := {type := review pi {op := syntax.atom {val := "Π"}, binders := bindrs, range := type.type}}}}
   | _ := no_expansion
@@ -482,7 +482,7 @@ def builtin_transformers : rbmap name transformer (<) := rbmap.from_list [
   (assume.name, assume.transform),
   (if.name, if.transform),
   (let.name, let.transform),
-  (constant.name, constant.transform),
+  (axiom.name, axiom.transform),
   (declaration.name, declaration.transform),
   (intro_rule.name, intro_rule.transform),
   (variable.name, variable.transform),

library/init/lean/parser/declaration.lean

@@ -147,8 +147,8 @@ node! declaration [
       name: ident_univ_params.parser, sig: opt_decl_sig.parser, val: decl_val.parser],
     «instance»: node! «instance» ["instance", name: ident_univ_params.parser?, sig: decl_sig.parser, val: decl_val.parser],
     «example»: node! «example» ["example", sig: decl_sig.parser, val: decl_val.parser],
-    «constant»: node! «constant» [
-      kw: node_choice! constant_keyword {"constant", "axiom"},
+    «axiom»: node! «axiom» [ -- CommentTo(Kha): -- replaced `constant with `axiom
+      kw: node_choice! constant_keyword {"axiom"},
       name: ident_univ_params.parser,
       sig: decl_sig.parser],
     «inductive»: node! «inductive» [try [«class»: (symbol "class")?, "inductive"],

library/init/lean/util.lean

@@ -10,7 +10,7 @@ namespace lean
 
 /-- Print and accumulate run time of `act` when option `profiler` is set to `true`. -/
 @[extern 5 "lean_lean_profileit"]
-constant profileit {α : Type} (category : @& string) (pos : @& position) (act : io α) : io α
+constant profileit {α : Type} (category : @& string) (pos : @& position) (act : io α) : io α := act
 def profileit_pure {α : Type} (category : string) (pos : position) (fn : unit → α) : io α :=
 profileit category pos $ io.lazy_pure fn
 

src/boot/init/io.cpp

@@ -16,6 +16,7 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64;
 #endif
 obj* l_io_prim_iterate__aux___main___boxed(obj*, obj*);
 obj* l_io_prim_iterate___at_io_prim_iterate__eio___spec__1(obj*, obj*, obj*, obj*);
+obj* l_io_prim_eio__inh___rarg___closed__1;
 obj* l_io_fs_handle_mk___rarg(obj*, obj*, obj*, obj*, obj*, uint8, uint8);
 obj* l_io_fs_handle_is__eof___at_io_fs_handle_read__to__end___spec__1(obj*, obj*);
 obj* l_io_println___at_io_println_x_27___spec__1(obj*, obj*);
@@ -33,6 +34,7 @@ obj* l_io_prim_io__inhabited(obj*);
 obj* l_io_fs_handle_flush___rarg(obj*, obj*, obj*, obj*, obj*);
 obj* l_io_has__eval___boxed(obj*);
 extern obj* l_string_iterator_extract___main___closed__1;
+obj* l___private_init_io_1__put__str___rarg(obj*, obj*, obj*, obj*, obj*);
 obj* l_io_prim_iterate___at_io_prim_iterate__eio___spec__1___boxed(obj*, obj*, obj*, obj*);
 obj* l_io_prim_handle_flush___boxed(obj*, obj*);
 obj* l_io_fs_handle_is__eof___rarg___lambda__1(obj*, obj*, obj*, obj*);
@@ -51,11 +53,10 @@ obj* l_io_prim_handle_is__eof___boxed(obj*, obj*);
 obj* l_io_prim_iterate___at_io_prim_iterate__eio___spec__1___rarg(obj*, obj*, obj*);
 obj* l_io_prim_handle_mk___boxed(obj*, obj*, obj*, obj*);
 obj* l_io_fs_read__file___rarg(obj*, obj*, obj*, obj*, obj*, uint8);
-obj* l___private_init_io_13__put__str___rarg(obj*, obj*, obj*, obj*, obj*);
 obj* l_io_prim_lift__eio(obj*, obj*, obj*);
 obj* l_io_prim_io__inhabited___boxed(obj*);
+obj* l_io_prim_eio__inh(obj*);
 obj* l_io_fs_handle_mk___boxed(obj*, obj*);
-obj* l___private_init_io_13__put__str___boxed(obj*, obj*);
 obj* l_io_fs_handle_is__eof___at_io_fs_handle_read__to__end___spec__1___boxed(obj*, obj*);
 obj* l_io_println_x_27___boxed(obj*, obj*);
 obj* l_allocprof___boxed(obj*, obj*, obj*, obj*);
@@ -69,9 +70,9 @@ namespace lean {
 obj* string_append(obj*, obj*);
 }
 obj* l_eio_has__eval(obj*, obj*);
-obj* l___private_init_io_13__put__str___at_io_println_x_27___spec__3(obj*, obj*);
 obj* l_io_print___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_io_fs_read__file___boxed(obj*, obj*);
+obj* l___private_init_io_1__put__str(obj*, obj*);
 obj* l_io_fs_handle_is__eof___boxed(obj*, obj*);
 obj* l_io_fs_read__file___rarg___lambda__2(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_io_fs_handle_read__to__end(obj*, obj*);
@@ -83,6 +84,7 @@ obj* l_io_prim_io__inhabited___rarg(obj*);
 obj* l_io_fs_read__file___rarg___lambda__3(obj*, obj*, obj*, obj*, obj*, obj*);
 extern "C" obj* lean_io_prim_handle_close(obj*, obj*);
 obj* l_io_lazy__pure___boxed(obj*);
+obj* l___private_init_io_1__put__str___at_io_println_x_27___spec__3___boxed(obj*, obj*);
 obj* l_io_prim_inhabited(obj*, obj*);
 obj* l_io_println___boxed(obj*, obj*);
 obj* l_io_prim_iterate(obj*, obj*, obj*);
@@ -92,7 +94,9 @@ obj* l_has__repr_has__eval(obj*);
 obj* l_io_println___rarg___closed__1;
 obj* l_io_print(obj*, obj*);
 obj* l_io_fs_handle_is__eof(obj*, obj*);
+obj* l___private_init_io_1__put__str___boxed(obj*, obj*);
 obj* l_io_prim_iterate___at_io_prim_iterate__eio___spec__1___rarg___lambda__1(obj*, obj*, obj*);
+obj* l_io_prim_eio__inh___boxed(obj*);
 obj* l_io_prim_inhabited___rarg(obj*);
 obj* l_io_fs_handle_close___rarg(obj*, obj*, obj*, obj*, obj*);
 extern "C" obj* lean_io_prim_handle_flush(obj*, obj*);
@@ -113,7 +117,6 @@ obj* l_eio__unit_has__eval___rarg(obj*, obj*, obj*);
 obj* l_io_prim_iterate__aux(obj*, obj*);
 extern "C" obj* lean_io_unsafe(obj*, obj*, obj*);
 obj* l_io_fs_read__file(obj*, obj*);
-obj* l___private_init_io_13__put__str___at_io_println_x_27___spec__3___boxed(obj*, obj*);
 obj* l_io_prim_lift__eio___boxed(obj*, obj*, obj*);
 obj* l_io_fs_handle_flush___boxed(obj*, obj*);
 obj* l_state__t_pure___at_io_prim_io__inhabited___spec__1(obj*);
@@ -126,7 +129,6 @@ obj* l_io_println_x_27(obj*, obj*);
 obj* l_io_lazy__pure___rarg(obj*, obj*);
 obj* l_io_error_inhabited;
 obj* l_io_fs_handle_read__to__end___rarg(obj*, obj*, obj*, obj*, obj*);
-obj* l___private_init_io_13__put__str(obj*, obj*);
 obj* l_io_prim_handle_close___boxed(obj*, obj*);
 obj* l_io_prim_iterate___at_io_fs_handle_read__to__end___spec__4(obj*, obj*, obj*);
 obj* l_id_bind___boxed(obj*, obj*);
@@ -142,6 +144,7 @@ obj* l_io_prim_inhabited___boxed(obj*, obj*);
 obj* l_io_fs_handle_close(obj*, obj*);
 obj* l_io_println___at_io_println_x_27___spec__1___boxed(obj*, obj*);
 obj* l_io__unit_has__eval(obj*, obj*);
+obj* l_io_prim_eio__inh___rarg(obj*);
 obj* l_state__t_pure___at_io_prim_io__inhabited___spec__1___boxed(obj*);
 extern "C" obj* lean_io_prim_handle_is_eof(obj*, obj*);
 obj* l_eio_has__eval___boxed(obj*, obj*);
@@ -150,6 +153,7 @@ obj* l_id_monad___lambda__2___boxed(obj*, obj*, obj*, obj*);
 obj* l_string_has__lift(obj*);
 obj* l_io_fs_handle_get__line(obj*, obj*);
 obj* l_id_monad___lambda__3___boxed(obj*, obj*, obj*, obj*);
+obj* l___private_init_io_1__put__str___at_io_println_x_27___spec__3(obj*, obj*);
 obj* l_io_prim_iterate__eio___at_io_fs_handle_read__to__end___spec__3(obj*, obj*, obj*);
 obj* l_io_prim_iterate__aux___main(obj*, obj*);
 obj* l_io_fs_read__file___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
@@ -671,6 +675,44 @@ lean::dec(x_2);
 return x_3;
 }
 }
+obj* _init_l_io_prim_eio__inh___rarg___closed__1() {
+_start:
+{
+obj* x_0; obj* x_1; 
+x_0 = lean::mk_string("");
+x_1 = lean::alloc_cnstr(0, 1, 0);
+lean::cnstr_set(x_1, 0, x_0);
+return x_1;
+}
+}
+obj* l_io_prim_eio__inh___rarg(obj* x_0) {
+_start:
+{
+obj* x_1; obj* x_2; 
+x_1 = l_io_prim_eio__inh___rarg___closed__1;
+x_2 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_2, 0, x_1);
+lean::cnstr_set(x_2, 1, x_0);
+return x_2;
+}
+}
+obj* l_io_prim_eio__inh(obj* x_0) {
+_start:
+{
+obj* x_1; 
+x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_io_prim_eio__inh___rarg), 1, 0);
+return x_1;
+}
+}
+obj* l_io_prim_eio__inh___boxed(obj* x_0) {
+_start:
+{
+obj* x_1; 
+x_1 = l_io_prim_eio__inh(x_0);
+lean::dec(x_0);
+return x_1;
+}
+}
 obj* l_io_prim_put__str___boxed(obj* x_0, obj* x_1) {
 _start:
 {
@@ -805,7 +847,7 @@ lean::dec(x_2);
 return x_3;
 }
 }
-obj* l___private_init_io_13__put__str___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
+obj* l___private_init_io_1__put__str___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
 _start:
 {
 obj* x_5; obj* x_6; obj* x_8; obj* x_9; obj* x_10; 
@@ -822,19 +864,19 @@ x_10 = lean::apply_4(x_6, lean::box(0), lean::box(0), x_8, x_9);
 return x_10;
 }
 }
-obj* l___private_init_io_13__put__str(obj* x_0, obj* x_1) {
+obj* l___private_init_io_1__put__str(obj* x_0, obj* x_1) {
 _start:
 {
 obj* x_2; 
-x_2 = lean::alloc_closure(reinterpret_cast<void*>(l___private_init_io_13__put__str___rarg), 5, 0);
+x_2 = lean::alloc_closure(reinterpret_cast<void*>(l___private_init_io_1__put__str___rarg), 5, 0);
 return x_2;
 }
 }
-obj* l___private_init_io_13__put__str___boxed(obj* x_0, obj* x_1) {
+obj* l___private_init_io_1__put__str___boxed(obj* x_0, obj* x_1) {
 _start:
 {
 obj* x_2; 
-x_2 = l___private_init_io_13__put__str(x_0, x_1);
+x_2 = l___private_init_io_1__put__str(x_0, x_1);
 lean::dec(x_0);
 lean::dec(x_1);
 return x_2;
@@ -845,7 +887,7 @@ _start:
 {
 obj* x_7; obj* x_8; 
 x_7 = lean::apply_1(x_5, x_6);
-x_8 = l___private_init_io_13__put__str___rarg(x_0, x_1, x_2, x_3, x_7);
+x_8 = l___private_init_io_1__put__str___rarg(x_0, x_1, x_2, x_3, x_7);
 return x_8;
 }
 }
@@ -899,7 +941,7 @@ lean::inc(x_1);
 lean::inc(x_0);
 x_16 = l_io_print___rarg(x_0, x_1, x_2, x_3, lean::box(0), x_5, x_6);
 x_17 = l_io_println___rarg___closed__1;
-x_18 = l___private_init_io_13__put__str___rarg(x_0, x_1, x_2, x_3, x_17);
+x_18 = l___private_init_io_1__put__str___rarg(x_0, x_1, x_2, x_3, x_17);
 x_19 = lean::apply_4(x_9, lean::box(0), lean::box(0), x_16, x_18);
 return x_19;
 }
@@ -1752,7 +1794,7 @@ lean::cnstr_set(x_7, 1, x_3);
 return x_7;
 }
 }
-obj* l___private_init_io_13__put__str___at_io_println_x_27___spec__3(obj* x_0, obj* x_1) {
+obj* l___private_init_io_1__put__str___at_io_println_x_27___spec__3(obj* x_0, obj* x_1) {
 _start:
 {
 obj* x_2; obj* x_3; 
@@ -1835,7 +1877,7 @@ obj* l_io_print___at_io_println_x_27___spec__2(obj* x_0, obj* x_1) {
 _start:
 {
 obj* x_2; 
-x_2 = l___private_init_io_13__put__str___at_io_println_x_27___spec__3(x_0, x_1);
+x_2 = l___private_init_io_1__put__str___at_io_println_x_27___spec__3(x_0, x_1);
 return x_2;
 }
 }
@@ -1843,7 +1885,7 @@ obj* l_io_println___at_io_println_x_27___spec__1(obj* x_0, obj* x_1) {
 _start:
 {
 obj* x_2; obj* x_3; 
-x_2 = l___private_init_io_13__put__str___at_io_println_x_27___spec__3(x_0, x_1);
+x_2 = l___private_init_io_1__put__str___at_io_println_x_27___spec__3(x_0, x_1);
 x_3 = lean::cnstr_get(x_2, 0);
 lean::inc(x_3);
 if (lean::obj_tag(x_3) == 0)
@@ -1889,7 +1931,7 @@ x_14 = lean::cnstr_get(x_2, 1);
 lean::inc(x_14);
 lean::dec(x_2);
 x_17 = l_io_println___rarg___closed__1;
-x_18 = l___private_init_io_13__put__str___at_io_println_x_27___spec__3(x_17, x_14);
+x_18 = l___private_init_io_1__put__str___at_io_println_x_27___spec__3(x_17, x_14);
 return x_18;
 }
 }
@@ -1919,11 +1961,11 @@ lean::cnstr_set(x_7, 1, x_3);
 return x_7;
 }
 }
-obj* l___private_init_io_13__put__str___at_io_println_x_27___spec__3___boxed(obj* x_0, obj* x_1) {
+obj* l___private_init_io_1__put__str___at_io_println_x_27___spec__3___boxed(obj* x_0, obj* x_1) {
 _start:
 {
 obj* x_2; 
-x_2 = l___private_init_io_13__put__str___at_io_println_x_27___spec__3(x_0, x_1);
+x_2 = l___private_init_io_1__put__str___at_io_println_x_27___spec__3(x_0, x_1);
 lean::dec(x_0);
 return x_2;
 }
@@ -2172,6 +2214,8 @@ lean::mark_persistent(l_io_monad);
 lean::mark_persistent(l_io_error_has__to__string);
  l_io_error_inhabited = _init_l_io_error_inhabited();
 lean::mark_persistent(l_io_error_inhabited);
+ l_io_prim_eio__inh___rarg___closed__1 = _init_l_io_prim_eio__inh___rarg___closed__1();
+lean::mark_persistent(l_io_prim_eio__inh___rarg___closed__1);
  l_io_println___rarg___closed__1 = _init_l_io_println___rarg___closed__1();
 lean::mark_persistent(l_io_println___rarg___closed__1);
  l_eio_has__eval___rarg___closed__1 = _init_l_eio_has__eval___rarg___closed__1();

src/boot/init/lean/elaborator.cpp

@@ -312,7 +312,6 @@ obj* l_reader__t_bind___at_lean_elaborator_declaration_elaborate___spec__1___rar
 obj* l_lean_elaborator_mk__notation__kind(obj*, obj*);
 obj* l_rbnode_ins___main___at_lean_elaborator_ordered__rbmap_insert___spec__4(obj*, obj*, obj*);
 extern "C" obj* level_mk_imax(obj*, obj*);
-obj* l_lean_environment_mk__empty___boxed(obj*);
 obj* l_lean_elaborator_ordered__rbmap_empty___at_lean_elaborator_old__elab__command___spec__15___boxed(obj*);
 obj* l_rbnode_ins___main___at_lean_elaborator_old__elab__command___spec__13___boxed(obj*, obj*, obj*, obj*);
 obj* l_lean_elaborator_attribute_elaborate___closed__2;
@@ -752,14 +751,6 @@ obj* l_lean_elaborator_init__quot_elaborate___closed__1;
 obj* l_lean_elaborator_postprocess__notation__spec___closed__1;
 obj* l_lean_elaborator_mk__state___closed__1;
 extern obj* l_lean_parser_command_set__option_has__view;
-obj* l_lean_environment_mk__empty___boxed(obj* x_0) {
-_start:
-{
-obj* x_1; 
-x_1 = lean_environment_mk_empty(x_0);
-return x_1;
-}
-}
 obj* l_lean_environment_contains___boxed(obj* x_0, obj* x_1) {
 _start:
 {
@@ -22636,7 +22627,7 @@ x_0 = lean::box(0);
 x_1 = lean::box(0);
 x_2 = lean::mk_string("command");
 x_3 = lean_name_mk_string(x_1, x_2);
-x_4 = lean::mk_string("constant");
+x_4 = lean::mk_string("axiom");
 x_5 = lean_name_mk_string(x_1, x_4);
 x_6 = l_lean_kvmap_set__name(x_0, x_3, x_5);
 return x_6;
@@ -22731,7 +22722,7 @@ lean::dec(x_17);
 x_34 = lean::cnstr_get(x_11, 0);
 lean::inc(x_34);
 lean::dec(x_11);
-x_37 = lean::mk_nat_obj(5u);
+x_37 = lean::mk_nat_obj(6u);
 x_38 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_elaborator_elab__def__like___boxed), 7, 4);
 lean::closure_set(x_38, 0, x_0);
 lean::closure_set(x_38, 1, x_34);
@@ -22779,7 +22770,7 @@ lean::cnstr_set(x_65, 1, x_46);
 lean::cnstr_set(x_65, 2, x_50);
 lean::cnstr_set(x_65, 3, x_60);
 lean::cnstr_set(x_65, 4, x_61);
-x_66 = lean::mk_nat_obj(3u);
+x_66 = lean::mk_nat_obj(4u);
 x_67 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_elaborator_elab__def__like___boxed), 7, 4);
 lean::closure_set(x_67, 0, x_0);
 lean::closure_set(x_67, 1, x_43);
@@ -22821,7 +22812,7 @@ lean::cnstr_set(x_90, 1, x_75);
 lean::cnstr_set(x_90, 2, x_89);
 lean::cnstr_set(x_90, 3, x_84);
 lean::cnstr_set(x_90, 4, x_85);
-x_91 = lean::mk_nat_obj(2u);
+x_91 = lean::mk_nat_obj(3u);
 x_92 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_elaborator_elab__def__like___boxed), 7, 4);
 lean::closure_set(x_92, 0, x_0);
 lean::closure_set(x_92, 1, x_72);

src/boot/init/lean/expander.cpp

@@ -39,7 +39,6 @@ obj* l_lean_expander_pi_transform___lambda__1(obj*, obj*, obj*);
 extern obj* l_lean_parser_term_binder__ident_has__view;
 obj* l_lean_expander_if_transform___closed__1;
 obj* l_list_map___main___at_lean_expander_expand__bracketed__binder___main___spec__4(uint8, obj*, obj*);
-extern obj* l_lean_parser_command_constant_has__view;
 obj* l_lean_expander_coe__simple__binder__binders(obj*);
 obj* l_list_map___main___at_lean_expander_expand__bracketed__binder___main___spec__19(obj*, obj*);
 obj* l_lean_expander_assume_transform___boxed(obj*, obj*);
@@ -89,7 +88,6 @@ obj* l_lean_parser_syntax_flip__scopes___main(obj*, obj*);
 obj* l_rbnode_ins___main___at_lean_expander_builtin__transformers___spec__4(obj*, obj*, obj*, obj*);
 obj* l_lean_expander_mixfix__to__notation__spec___boxed(obj*, obj*, obj*);
 obj* l_lean_expander_error___rarg___lambda__1___closed__1;
-obj* l_lean_expander_constant_transform___boxed(obj*, obj*);
 obj* l_list_map___main___at_lean_expander_coe__binders__ext___spec__2___boxed(obj*);
 obj* l_lean_expander_assume_transform___closed__1;
 obj* l_list_foldr___main___at_lean_expander_expand__binders___spec__7(obj*, obj*, obj*);
@@ -111,6 +109,7 @@ uint8 l_lean_parser_syntax_is__of__kind___main(obj*, obj*);
 obj* l_list_foldr___main___at_lean_expander_expand__binders___spec__8___boxed(obj*, obj*, obj*);
 obj* l_lean_expander_transform__m_monad;
 obj* l_lean_expander_expand__bracketed__binder___main___closed__4;
+extern obj* l_lean_parser_command_axiom_has__view;
 obj* l_lean_expander_error___at___private_init_lean_expander_1__pop__stx__arg___spec__1___rarg___boxed(obj*, obj*, obj*, obj*);
 extern obj* l_lean_parser_command_variable_has__view;
 obj* l_lean_expander_arrow_transform___closed__1;
@@ -126,6 +125,7 @@ obj* l_lean_expander_if_transform___closed__3;
 obj* l_lean_expander_if_transform___boxed(obj*, obj*);
 obj* l_lean_expander_expander__config_has__lift___boxed(obj*);
 extern obj* l_lean_parser_term_pi_has__view;
+obj* l_list_map___main___at_lean_expander_axiom_transform___spec__1(obj*);
 extern obj* l_lean_parser_command_universe_has__view;
 obj* l_lean_expander_error___at_lean_expander_mk__notation__transformer___spec__1(obj*);
 extern obj* l_lean_parser_ident__univs;
@@ -200,6 +200,7 @@ extern obj* l_lean_parser_term__parser__m_lean_parser_monad__parsec;
 obj* l_list_map___main___at_lean_expander_expand__bracketed__binder___main___spec__2(uint8, obj*, obj*);
 obj* l_lean_expander_error___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_lean_expander_binding__annotation__update;
+obj* l_lean_expander_axiom_transform___closed__1;
 extern obj* l_lean_parser_term__parser__m_monad;
 extern obj* l_lean_parser_term_let_has__view;
 obj* l_lean_expander_transform__m_monad__reader;
@@ -230,6 +231,7 @@ obj* l_rbnode_ins___main___at_lean_expander_builtin__transformers___spec__5___bo
 obj* l_lean_expander_no__expansion(obj*);
 obj* l_lean_expander_binding__annotation__update_has__view_x_27___lambda__1___closed__1;
 obj* l_lean_parser_syntax_mk__node(obj*, obj*);
+obj* l_lean_expander_axiom_transform(obj*, obj*);
 obj* l_lean_expander_declaration_transform___closed__2;
 obj* l_rbnode_balance2___main___rarg(obj*, obj*);
 obj* l_lean_expander_get__opt__type___main(obj*);
@@ -275,6 +277,7 @@ extern "C" uint8 lean_name_dec_eq(obj*, obj*);
 obj* l_lean_expander_error___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_list_map___main___at_lean_expander_expand__bracketed__binder___main___spec__18(obj*, obj*);
 obj* l_lean_expander_declaration_transform___closed__1;
+obj* l_lean_expander_axiom_transform___boxed(obj*, obj*);
 obj* l_lean_expander_error___at_lean_expander_mk__notation__transformer___spec__1___boxed(obj*);
 uint8 l_lean_name_quick__lt(obj*, obj*);
 obj* l_lean_expander_coe__binders__ext__binders(obj*);
@@ -291,6 +294,7 @@ obj* l_list_foldr___main___at_lean_expander_expand__binders___spec__4___boxed(ob
 obj* l_list_map___main___at_lean_expander_expand__bracketed__binder___main___spec__15(obj*, obj*);
 obj* l_lean_expander_binder__ident__to__ident___main___boxed(obj*);
 obj* l_lean_expander_transformer__config__coe__frontend__config(obj*);
+extern obj* l_lean_parser_command_axiom;
 obj* l_lean_expander_expand__bracketed__binder___main(obj*, obj*);
 obj* l_lean_expander_binding__annotation__update_has__view_x_27___lambda__1(obj*);
 obj* l_string_trim(obj*);
@@ -298,7 +302,6 @@ obj* l_lean_expander_variable_transform___closed__1;
 obj* l_list_map___main___at_lean_expander_mk__notation__transformer___spec__5(obj*);
 obj* l_list_map___main___at_lean_expander_expand__bracketed__binder___main___spec__13(obj*, obj*);
 obj* l_lean_expander_error___rarg___lambda__1(obj*, obj*, obj*, obj*, obj*);
-extern obj* l_lean_parser_command_constant;
 obj* l_lean_expander_paren_transform___closed__2;
 extern obj* l_lean_parser_term_if;
 extern obj* l_lean_parser_term_assume;
@@ -314,7 +317,6 @@ obj* l___private_init_lean_expander_2__expand__core___main(obj*, obj*, obj*, obj
 obj* l_lean_expander_assume_transform(obj*, obj*);
 obj* l_lean_parser_syntax_mreplace___main___at_lean_parser_syntax_replace___spec__1(obj*, obj*);
 obj* l_list_map___main___at_lean_expander_expand__bracketed__binder___main___spec__17(obj*, obj*);
-obj* l_list_map___main___at_lean_expander_constant_transform___spec__1(obj*);
 obj* l_lean_expander_mk__simple__binder___closed__1;
 extern obj* l_lean_parser_command_notation__spec_precedence_has__view;
 obj* l_lean_expander_variable_transform(obj*, obj*);
@@ -349,7 +351,6 @@ obj* l_list_foldr___main___at_lean_expander_expand__binders___spec__5(obj*, obj*
 obj* l_dlist_singleton___rarg(obj*, obj*);
 obj* l_lean_expander_get__opt__type___main___closed__1;
 obj* l_list_mfoldr___main___at_lean_expander_expand__binders___spec__9___closed__3;
-obj* l_lean_expander_constant_transform___closed__1;
 obj* l_lean_expander_mixfix__to__notation__spec___closed__4;
 obj* l_lean_parser_combinators_node___at_lean_parser_command_notation__spec_precedence__lit_parser___spec__1(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_list_map___main___at_lean_expander_expand__bracketed__binder___main___spec__1___boxed(obj*, obj*, obj*);
@@ -373,7 +374,6 @@ obj* l_list_map___main___at___private_init_lean_expander_2__expand__core___main_
 obj* l_list_mmap___main___at_lean_expander_variables_transform___spec__1(obj*, obj*);
 obj* l_id_monad___lambda__3___boxed(obj*, obj*, obj*, obj*);
 obj* l_list_map___main___at_lean_expander_expand__bracketed__binder___main___spec__4___boxed(obj*, obj*, obj*);
-obj* l_lean_expander_constant_transform(obj*, obj*);
 obj* l_lean_expander_binder__ident__to__ident___boxed(obj*);
 obj* l_list_map___main___at_lean_expander_expand__bracketed__binder___main___spec__11(obj*, obj*);
 obj* l_rbnode_set__black___main___rarg(obj*);
@@ -8886,7 +8886,7 @@ lean::dec(x_1);
 return x_2;
 }
 }
-obj* l_list_map___main___at_lean_expander_constant_transform___spec__1(obj* x_0) {
+obj* l_list_map___main___at_lean_expander_axiom_transform___spec__1(obj* x_0) {
 _start:
 {
 if (lean::obj_tag(x_0) == 0)
@@ -8910,7 +8910,7 @@ if (lean::is_exclusive(x_0)) {
 }
 x_7 = lean::alloc_cnstr(0, 1, 0);
 lean::cnstr_set(x_7, 0, x_2);
-x_8 = l_list_map___main___at_lean_expander_constant_transform___spec__1(x_4);
+x_8 = l_list_map___main___at_lean_expander_axiom_transform___spec__1(x_4);
 if (lean::is_scalar(x_6)) {
  x_9 = lean::alloc_cnstr(1, 2, 0);
 } else {
@@ -8922,7 +8922,7 @@ return x_9;
 }
 }
 }
-obj* _init_l_lean_expander_constant_transform___closed__1() {
+obj* _init_l_lean_expander_axiom_transform___closed__1() {
 _start:
 {
 obj* x_0; obj* x_1; 
@@ -8932,11 +8932,11 @@ lean::cnstr_set(x_1, 0, x_0);
 return x_1;
 }
 }
-obj* l_lean_expander_constant_transform(obj* x_0, obj* x_1) {
+obj* l_lean_expander_axiom_transform(obj* x_0, obj* x_1) {
 _start:
 {
 obj* x_2; obj* x_3; obj* x_5; obj* x_6; obj* x_8; 
-x_2 = l_lean_parser_command_constant_has__view;
+x_2 = l_lean_parser_command_axiom_has__view;
 x_3 = lean::cnstr_get(x_2, 0);
 lean::inc(x_3);
 x_5 = lean::apply_1(x_3, x_0);
@@ -8960,7 +8960,7 @@ x_13 = lean::cnstr_get(x_8, 0);
 lean::inc(x_13);
 lean::dec(x_8);
 x_16 = lean::box(0);
-x_17 = l_list_map___main___at_lean_expander_constant_transform___spec__1(x_13);
+x_17 = l_list_map___main___at_lean_expander_axiom_transform___spec__1(x_13);
 x_18 = lean::alloc_cnstr(1, 1, 0);
 lean::cnstr_set(x_18, 0, x_17);
 x_19 = lean::alloc_cnstr(1, 1, 0);
@@ -9003,7 +9003,7 @@ x_41 = l_lean_expander_mk__simple__binder___closed__1;
 x_42 = lean::alloc_cnstr(0, 2, 0);
 lean::cnstr_set(x_42, 0, x_41);
 lean::cnstr_set(x_42, 1, x_40);
-x_43 = l_lean_expander_constant_transform___closed__1;
+x_43 = l_lean_expander_axiom_transform___closed__1;
 if (lean::is_scalar(x_12)) {
  x_44 = lean::alloc_cnstr(0, 2, 0);
 } else {
@@ -9037,11 +9037,11 @@ return x_52;
 }
 }
 }
-obj* l_lean_expander_constant_transform___boxed(obj* x_0, obj* x_1) {
+obj* l_lean_expander_axiom_transform___boxed(obj* x_0, obj* x_1) {
 _start:
 {
 obj* x_2; 
-x_2 = l_lean_expander_constant_transform(x_0, x_1);
+x_2 = l_lean_expander_axiom_transform(x_0, x_1);
 lean::dec(x_1);
 return x_2;
 }
@@ -9535,7 +9535,7 @@ lean::cnstr_set(x_51, 0, x_50);
 lean::cnstr_set(x_51, 1, x_49);
 x_52 = lean::alloc_cnstr(1, 1, 0);
 lean::cnstr_set(x_52, 0, x_51);
-x_53 = l_lean_expander_constant_transform___closed__1;
+x_53 = l_lean_expander_axiom_transform___closed__1;
 if (lean::is_scalar(x_12)) {
  x_54 = lean::alloc_cnstr(0, 2, 0);
 } else {
@@ -11041,8 +11041,8 @@ x_28 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_expander_let_transform
 x_29 = lean::alloc_cnstr(0, 2, 0);
 lean::cnstr_set(x_29, 0, x_27);
 lean::cnstr_set(x_29, 1, x_28);
-x_30 = l_lean_parser_command_constant;
-x_31 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_expander_constant_transform___boxed), 2, 0);
+x_30 = l_lean_parser_command_axiom;
+x_31 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_expander_axiom_transform___boxed), 2, 0);
 x_32 = lean::alloc_cnstr(0, 2, 0);
 lean::cnstr_set(x_32, 0, x_30);
 lean::cnstr_set(x_32, 1, x_31);
@@ -12134,8 +12134,8 @@ lean::mark_persistent(l_lean_expander_if_transform___closed__2);
 lean::mark_persistent(l_lean_expander_if_transform___closed__3);
  l_lean_expander_let_transform___closed__1 = _init_l_lean_expander_let_transform___closed__1();
 lean::mark_persistent(l_lean_expander_let_transform___closed__1);
- l_lean_expander_constant_transform___closed__1 = _init_l_lean_expander_constant_transform___closed__1();
-lean::mark_persistent(l_lean_expander_constant_transform___closed__1);
+ l_lean_expander_axiom_transform___closed__1 = _init_l_lean_expander_axiom_transform___closed__1();
+lean::mark_persistent(l_lean_expander_axiom_transform___closed__1);
  l_lean_expander_declaration_transform___closed__1 = _init_l_lean_expander_declaration_transform___closed__1();
 lean::mark_persistent(l_lean_expander_declaration_transform___closed__1);
  l_lean_expander_declaration_transform___closed__2 = _init_l_lean_expander_declaration_transform___closed__2();

src/boot/init/lean/frontend.cpp

@@ -14,7 +14,7 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64;
 #pragma GCC diagnostic ignored "-Wunused-label"
 #pragma GCC diagnostic ignored "-Wunused-but-set-variable"
 #endif
-obj* l___private_init_io_13__put__str___at_lean_process__file___spec__3___boxed(obj*, obj*);
+obj* l___private_init_io_1__put__str___at_lean_process__file___spec__3(obj*, obj*);
 obj* l_io_prim_iterate__aux___rarg(obj*, obj*, obj*, obj*);
 obj* l_list_mmap_x_27___main___at_lean_run__frontend___spec__2(obj*, obj*, obj*);
 obj* l_lean_run__frontend___boxed(obj*, obj*, obj*, obj*, obj*);
@@ -56,7 +56,6 @@ obj* l_lean_parser_tokens___rarg(obj*);
 extern obj* l_lean_parser_module_eoi;
 obj* l_io_println___at_lean_process__file___spec__1___boxed(obj*, obj*);
 extern obj* l_lean_format_be___main___closed__1;
-obj* l___private_init_io_13__put__str___at_lean_process__file___spec__3(obj*, obj*);
 obj* l_io_prim_iterate___at_lean_run__frontend___spec__6___lambda__1___boxed(obj*, obj*, obj*);
 obj* l_io_prim_iterate___at_lean_run__frontend___spec__6___lambda__4___closed__2;
 obj* l_io_print___at_lean_process__file___spec__2___boxed(obj*, obj*);
@@ -70,6 +69,7 @@ obj* l_io_prim_iterate___at_lean_run__frontend___spec__6___lambda__2___boxed(obj
 obj* l_lean_message_to__string(obj*);
 obj* l_lean_process__file___lambda__1___closed__7;
 obj* l_io_prim_iterate___at_lean_run__frontend___spec__6___lambda__4___closed__3;
+obj* l___private_init_io_1__put__str___at_lean_process__file___spec__3___boxed(obj*, obj*);
 obj* l_lean_file__map_from__string(obj*);
 extern obj* l_lean_parser_module_header_parser_lean_parser_has__tokens;
 obj* l_lean_process__file___boxed(obj*, obj*, obj*, obj*);
@@ -1766,7 +1766,7 @@ x_6 = l_lean_run__frontend(x_0, x_1, x_2, x_5, x_4);
 return x_6;
 }
 }
-obj* l___private_init_io_13__put__str___at_lean_process__file___spec__3(obj* x_0, obj* x_1) {
+obj* l___private_init_io_1__put__str___at_lean_process__file___spec__3(obj* x_0, obj* x_1) {
 _start:
 {
 obj* x_2; obj* x_3; 
@@ -1849,7 +1849,7 @@ obj* l_io_print___at_lean_process__file___spec__2(obj* x_0, obj* x_1) {
 _start:
 {
 obj* x_2; 
-x_2 = l___private_init_io_13__put__str___at_lean_process__file___spec__3(x_0, x_1);
+x_2 = l___private_init_io_1__put__str___at_lean_process__file___spec__3(x_0, x_1);
 return x_2;
 }
 }
@@ -1857,7 +1857,7 @@ obj* l_io_println___at_lean_process__file___spec__1(obj* x_0, obj* x_1) {
 _start:
 {
 obj* x_2; obj* x_3; 
-x_2 = l___private_init_io_13__put__str___at_lean_process__file___spec__3(x_0, x_1);
+x_2 = l___private_init_io_1__put__str___at_lean_process__file___spec__3(x_0, x_1);
 x_3 = lean::cnstr_get(x_2, 0);
 lean::inc(x_3);
 if (lean::obj_tag(x_3) == 0)
@@ -1903,7 +1903,7 @@ x_14 = lean::cnstr_get(x_2, 1);
 lean::inc(x_14);
 lean::dec(x_2);
 x_17 = l_lean_format_be___main___closed__1;
-x_18 = l___private_init_io_13__put__str___at_lean_process__file___spec__3(x_17, x_14);
+x_18 = l___private_init_io_1__put__str___at_lean_process__file___spec__3(x_17, x_14);
 return x_18;
 }
 }
@@ -2243,11 +2243,11 @@ return x_58;
 }
 }
 }
-obj* l___private_init_io_13__put__str___at_lean_process__file___spec__3___boxed(obj* x_0, obj* x_1) {
+obj* l___private_init_io_1__put__str___at_lean_process__file___spec__3___boxed(obj* x_0, obj* x_1) {
 _start:
 {
 obj* x_2; 
-x_2 = l___private_init_io_13__put__str___at_lean_process__file___spec__3(x_0, x_1);
+x_2 = l___private_init_io_1__put__str___at_lean_process__file___spec__3(x_0, x_1);
 lean::dec(x_0);
 return x_2;
 }

src/frontends/lean/decl_cmds.cpp

@@ -90,7 +90,6 @@ static environment declare_var(parser & p, environment env,
         p.add_variable(n, l);
         return env;
     } else {
-        lean_assert(k == variable_kind::Constant || k == variable_kind::Axiom);
         name const & ns = get_namespace(env);
         name full_n  = ns + n;
 
@@ -114,10 +113,6 @@ static environment declare_var(parser & p, environment env,
         env = ensure_decl_namespaces(env, full_n);
         /* Apply attributes last so that they may access any information on the new decl */
         env = meta.m_attrs.apply(env, p.ios(), full_n);
-        if (k == variable_kind::Constant) {
-            /* We need to invoke the compiler and generate boxed version if needed. */
-            env = compile(env, p.get_options(), names(full_n));
-        }
         return env;
     }
 }
@@ -137,8 +132,8 @@ optional<binder_info> parse_binder_info(parser & p, variable_kind k) {
 
 static void check_variable_kind(parser & p, variable_kind k) {
     if (in_section(p.env())) {
-        if (k == variable_kind::Axiom || k == variable_kind::Constant)
-            throw parser_error("invalid declaration, 'constant/axiom' cannot be used in sections",
+        if (k == variable_kind::Axiom)
+            throw parser_error("invalid declaration, 'axiom' cannot be used in sections",
                                p.pos());
     }
 }
@@ -157,7 +152,7 @@ static bool curr_is_binder_annotation(parser & p) {
            p.curr_is_token(get_ldcurly_tk()) || p.curr_is_token(get_lbracket_tk());
 }
 
-/* Auxiliary class to setup naming scopes for a variable/constant/axiom command.
+/* Auxiliary class to setup naming scopes for a variable/axiom command.
 
    We need the private_name_scope because the type may contain match-expressions.
    These match expressions produce private definitions, and we need to make sure
@@ -250,8 +245,8 @@ static environment variable_cmd_core(parser & p, variable_kind k, cmd_meta const
         var_decl_scope var_scope(p, meta.m_modifiers);
         /* non instance implicit cases */
         if (p.curr_is_token(get_lcurly_tk()) && (k == variable_kind::Variable))
-            throw parser_error("invalid declaration, only constants/axioms can be universe polymorphic", p.pos());
-        if (k == variable_kind::Constant || k == variable_kind::Axiom)
+            throw parser_error("invalid declaration, only axioms can be universe polymorphic", p.pos());
+        if (k == variable_kind::Axiom)
             scope1.emplace(p);
         parse_univ_params(p, ls_buffer);
         n = p.check_decl_id_next("invalid declaration, identifier expected");
@@ -285,9 +280,6 @@ static environment variable_cmd(parser & p, cmd_meta const & meta) {
 static environment axiom_cmd(parser & p, cmd_meta const & meta)    {
     return variable_cmd_core(p, variable_kind::Axiom, meta);
 }
-static environment constant_cmd(parser & p, cmd_meta const & meta)    {
-    return variable_cmd_core(p, variable_kind::Constant, meta);
-}
 
 /*
 Remark: we currently do not support declarations such as:
@@ -303,7 +295,7 @@ instead.
 */
 static void ensure_no_match_in_variables_cmd(pos_info const & pos) {
     if (used_match_idx()) {
-        throw parser_error("match-expressions are not supported in `variables/constants` commands", pos);
+        throw parser_error("match-expressions are not supported in `variables` commands", pos);
     }
 }
 
@@ -376,10 +368,10 @@ static environment variables_cmd_core(parser & p, variable_kind k, cmd_meta cons
                 else
                     return p.env();
             } else {
-                throw parser_error("invalid variables/constants/axioms declaration, ':' expected", pos);
+                throw parser_error("invalid variables declaration, ':' expected", pos);
             }
         }
-        if (k == variable_kind::Constant || k == variable_kind::Axiom)
+        if (k == variable_kind::Axiom)
             scope1.emplace(p);
         type = p.parse_expr();
         ensure_no_match_in_variables_cmd(pos);
@@ -401,34 +393,22 @@ static environment variables_cmd_core(parser & p, variable_kind k, cmd_meta cons
         env = declare_var(p, env, id, new_ls, new_type, k, bi, pos, meta);
     }
     if (curr_is_binder_annotation(p)) {
-        if (k == variable_kind::Constant || k == variable_kind::Axiom) {
-            // Hack: temporarily update the parser environment.
-            // We must do that to be able to process
-            //    constants (A : Type) (a : A)
-            parser::local_scope scope2(p, env);
-            return variables_cmd_core(p, k, meta);
-        } else {
-            return variables_cmd_core(p, k, meta);
-        }
+        return variables_cmd_core(p, k, meta);
     }
     return env;
 }
 static environment variables_cmd(parser & p, cmd_meta const & meta) {
     return variables_cmd_core(p, variable_kind::Variable, meta);
 }
-static environment constants_cmd(parser & p, cmd_meta const & meta) {
-    return variables_cmd_core(p, variable_kind::Constant, meta);
-}
-static environment axioms_cmd(parser & p, cmd_meta const & meta) {
-    return variables_cmd_core(p, variable_kind::Axiom, meta);
-}
-
 static environment definition_cmd(parser & p, cmd_meta const & meta) {
     return definition_cmd_core(p, decl_cmd_kind::Definition, meta);
 }
 static environment theorem_cmd(parser & p, cmd_meta const & meta) {
     return definition_cmd_core(p, decl_cmd_kind::Theorem, meta);
 }
+static environment constant_cmd(parser & p, cmd_meta const & meta) {
+    return definition_cmd_core(p, decl_cmd_kind::OpaqueConst, meta);
+}
 static environment abbreviation_cmd(parser & p, cmd_meta const & meta) {
     return definition_cmd_core(p, decl_cmd_kind::Abbreviation, meta);
 }
@@ -559,10 +539,8 @@ void register_decl_cmds(cmd_table & r) {
     add_cmd(r, cmd_info("universes",       "declare universe levels", universes_cmd));
     add_cmd(r, cmd_info("variable",        "declare a new variable", variable_cmd));
     add_cmd(r, cmd_info("constant",        "declare a new constant (aka top-level variable)", constant_cmd));
-    add_cmd(r, cmd_info("axiom",           "declare a new axiom", axiom_cmd));
     add_cmd(r, cmd_info("variables",       "declare new variables", variables_cmd));
-    add_cmd(r, cmd_info("constants",       "declare new constants (aka top-level variables)", constants_cmd));
-    add_cmd(r, cmd_info("axioms",          "declare new axioms", axioms_cmd));
+    add_cmd(r, cmd_info("axiom",           "declare a new axiom", axiom_cmd));
     add_cmd(r, cmd_info("unsafe",          "add new unsafe declaration", modifiers_cmd, false));
     add_cmd(r, cmd_info("mutual",          "add new mutual declaration", modifiers_cmd, false));
     add_cmd(r, cmd_info("noncomputable",   "add new noncomputable definition", modifiers_cmd, false));

src/frontends/lean/decl_cmds.h

@@ -22,7 +22,7 @@ bool parse_univ_params(parser & p, buffer<name> & ps);
     Then sort \c ls_buffer (using the order in which the universe levels were declared). */
 void update_univ_parameters(buffer<name> & ls_buffer, name_set const & found_ls, parser const & p);
 
-enum class variable_kind { Constant, Variable, Axiom };
+enum class variable_kind { Variable, Axiom };
 
 environment elab_var(parser & p, variable_kind const & k, cmd_meta const & meta, pos_info const & pos,
                      optional <binder_info> const & bi, name const & n, expr type, buffer <name> & ls_buffer);

src/frontends/lean/decl_util.h

@@ -14,7 +14,7 @@ struct parser;
 struct cmd_meta;
 class elaborator;
 
-enum class decl_cmd_kind { Theorem, Definition, Example, Instance, Var, Abbreviation };
+enum class decl_cmd_kind { Theorem, Definition, OpaqueConst, Example, Instance, Var, Abbreviation };
 
 struct decl_modifiers {
     bool m_is_private{false};

src/frontends/lean/definition_cmds.cpp

@@ -183,8 +183,7 @@ static environment compile_decl(parser & p, environment const & env,
 
 static pair<environment, name>
 declare_definition(environment const & env, decl_cmd_kind kind, buffer<name> const & lp_names,
-                   name const & c_name, name const & prv_name, expr type, optional<expr> val, cmd_meta const & meta,
-                   bool is_abbrev) {
+                   name const & c_name, name const & prv_name, expr type, optional<expr> val, cmd_meta const & meta) {
     name c_real_name;
     environment new_env = env;
     if (has_private_prefix(new_env, prv_name)) {
@@ -201,12 +200,17 @@ declare_definition(environment const & env, decl_cmd_kind kind, buffer<name> con
         std::tie(new_env, type) = abstract_nested_proofs(new_env, c_real_name, type);
         std::tie(new_env, *val) = abstract_nested_proofs(new_env, c_real_name, *val);
     }
-    bool is_meta      = meta.m_modifiers.m_is_unsafe;
-    auto def          =
-        (kind == decl_cmd_kind::Theorem ?
-         mk_theorem(c_real_name, names(lp_names), type, *val) :
-         (is_abbrev ? mk_definition(c_real_name, names(lp_names), type, *val, reducibility_hints::mk_abbreviation(), is_meta) :
-          mk_definition(new_env, c_real_name, names(lp_names), type, *val, is_meta)));
+    bool is_unsafe      = meta.m_modifiers.m_is_unsafe;
+    declaration def;
+    switch (kind) {
+    case decl_cmd_kind::Theorem:      def = mk_theorem(c_real_name, names(lp_names), type, *val); break;
+    case decl_cmd_kind::Abbreviation: def = mk_definition(c_real_name, names(lp_names), type, *val, reducibility_hints::mk_abbreviation(), is_unsafe); break;
+    case decl_cmd_kind::OpaqueConst:  def = mk_opaque(c_real_name, names(lp_names), type, *val); break;
+    case decl_cmd_kind::Instance:
+    case decl_cmd_kind::Definition:   def = mk_definition(new_env, c_real_name, names(lp_names), type, *val, is_unsafe); break;
+    default:
+        throw exception("unknown command declaration");
+    }
     new_env           = module::add(new_env, def);
 
     if (meta.m_modifiers.m_is_protected)
@@ -254,9 +258,8 @@ static environment elab_defs_core(parser & p, decl_cmd_kind kind, cmd_meta const
         environment env = elab.env();
         name c_name = local_name_p(fns[i]);
         name c_real_name;
-        bool is_abbrev = false;
         std::tie(env, c_real_name) = declare_definition(env, kind, lp_names, c_name, prv_names[i],
-                                                        curr_type, some_expr(curr), meta, is_abbrev);
+                                                        curr_type, some_expr(curr), meta);
         env = add_local_ref(p, env, c_name, c_real_name, lp_names, params);
         new_d_names.push_back(c_real_name);
         elab.set_env(env);
@@ -300,7 +303,7 @@ static environment mutual_definition_cmd_core(parser & p, decl_cmd_kind kind, cm
      Note that mlocal_pp_name_p(fn) and actual_name are different for scoped/private declarations.
 */
 static std::tuple<expr, expr, name> parse_definition(parser & p, buffer<name> & lp_names, buffer<expr> & params,
-                                                     bool is_example, bool is_instance, bool is_meta, bool is_abbrev) {
+                                                     bool is_example, bool is_instance, bool is_unsafe, bool is_abbrev) {
     parser::local_scope scope1(p);
     auto header_pos = p.pos();
     time_task _("parsing", p.mk_message(header_pos, INFORMATION));
@@ -309,7 +312,7 @@ static std::tuple<expr, expr, name> parse_definition(parser & p, buffer<name> &
     expr val;
     if (p.curr_is_token(get_assign_tk())) {
         p.next();
-        if (is_meta) {
+        if (is_unsafe) {
             declaration_name_scope scope2("_main");
             fn = mk_local(local_name_p(fn), local_pp_name_p(fn), local_type_p(fn), mk_rec_info());
             p.add_local(fn);
@@ -472,9 +475,9 @@ static void check_example(environment const & decl_env, options const & opts,
         buffer<name> univ_params_buf; to_buffer(univ_params, univ_params_buf);
         finalize_definition(elab, params_buf, type, val, univ_params_buf);
 
-        bool is_meta      = modifiers.m_is_unsafe;
+        bool is_unsafe      = modifiers.m_is_unsafe;
         auto new_env = elab.env();
-        declaration def = mk_definition(new_env, decl_name, names(univ_params_buf), type, val, is_meta);
+        declaration def = mk_definition(new_env, decl_name, names(univ_params_buf), type, val, is_unsafe);
         new_env = module::add(new_env, def);
     } catch (throwable & ex) {
         message_builder error_msg(tc, decl_env, get_global_ios(),
@@ -534,7 +537,7 @@ static environment elab_single_def(parser & p, decl_cmd_kind const & kind, cmd_m
             opt_val = elaborate_proof(decl_env, opts, header_pos, new_params_list,
                                       new_fn, val, thm_finfo, is_rfl, type,
                                       mctx, lctx, pos_provider, use_info_manager, file_name);
-            env_n = declare_definition(elab.env(), kind, lp_names, c_name, prv_name, type, opt_val, meta, is_abbrev);
+            env_n = declare_definition(elab.env(), kind, lp_names, c_name, prv_name, type, opt_val, meta);
         } else if (kind == decl_cmd_kind::Example) {
             auto env = p.env();
             auto opts = p.get_options();
@@ -559,7 +562,7 @@ static environment elab_single_def(parser & p, decl_cmd_kind const & kind, cmd_m
                 val = get_equations_result(val, 0);
             }
             finalize_definition(elab, new_params, type, val, lp_names);
-            env_n = declare_definition(elab.env(), kind, lp_names, c_name, prv_name, type, some_expr(val), meta, is_abbrev);
+            env_n = declare_definition(elab.env(), kind, lp_names, c_name, prv_name, type, some_expr(val), meta);
         }
         time_task _("decl post-processing", p.mk_message(header_pos, INFORMATION), c_name);
         environment new_env = env_n.first;

src/frontends/lean/token_table.cpp

@@ -101,10 +101,9 @@ void init_token_table(token_table & t) {
          {"node_longest_choice!", g_max_prec}, {nullptr, 0}};
 
     char const * commands[] =
-        {"theorem", "axiom", "axioms", "variable", "protected", "private", "hide",
+        {"theorem", "axiom", "variable", "protected", "private", "hide",
          "definition", "unsafe", "mutual", "example", "noncomputable", "abbreviation", "abbrev",
-         "variables", "constant", "constants",
-         "using_well_founded", "[whnf]",
+         "variables", "constant", "using_well_founded", "[whnf]",
          "end", "namespace", "section", "prelude",
          "import", "inductive", "coinductive", "structure", "class", "universe", "universes", "local",
          "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation",

src/frontends/lean/vm_elaborator.cpp

@@ -227,14 +227,14 @@ expr const & get_arg_names(expr const & e, buffer<name> & ns) {
     return fn;
 }
 
-void elab_constant_cmd(parser & p, expr const & cmd) {
+void elab_axiom_cmd(parser & p, expr const & cmd) {
     buffer<expr> args;
     buffer<name> ls;
     get_app_args(mdata_expr(cmd), args);
     auto fn = get_arg_names(args[1], ls);
     expr type = args[2];
     type = resolve_names(p, type);
-    p.set_env(elab_var(p, variable_kind::Constant, to_cmd_meta(p.env(), args[0]), get_pos_info_provider()->get_pos_info_or_some(cmd),
+    p.set_env(elab_var(p, variable_kind::Axiom, to_cmd_meta(p.env(), args[0]), get_pos_info_provider()->get_pos_info_or_some(cmd),
                        optional<binder_info>(), const_name(fn), type, ls));
 }
 
@@ -385,8 +385,8 @@ static void elaborate_command(parser & p, expr const & cmd) {
         } else if (*cmd_name == "#check") {
             elab_check_cmd(p, cmd);
             return;
-        } else if (*cmd_name == "constant") {
-            elab_constant_cmd(p, cmd);
+        } else if (*cmd_name == "axiom") {
+            elab_axiom_cmd(p, cmd);
             return;
         } else if (*cmd_name == "defs") {
             elab_defs_cmd(p, cmd);