max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/init/meta/level): make level as meta

Browse source
This commit is contained in:
Leonardo de Moura 2017-06-06 16:12:35 -07:00
parent 3bc414efff
commit 9b60e25ca4
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/meta/level.lean
View file

@ -7,7 +7,7 @@ prelude
import init.meta.name init.meta.format
/- Reflect a C++ level object. The VM replaces it with the C++ implementation. -/
inductive level
meta inductive level
| zero : level
| succ : level → level
| max : level → level → level
@ -15,7 +15,7 @@ inductive level
| param : name → level
| mvar : name → level
instance : inhabited level :=
meta instance : inhabited level :=
⟨level.zero⟩
/- TODO(Leo): provide a definition in Lean. -/