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

feat(library/init/lean/declaration): use task at theorem and definition declaration objects

Browse source
This commit is contained in:
Leonardo de Moura 2018-08-22 10:31:50 -07:00
parent d0dc998873
commit d64a49a7da
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/init/lean/declaration.lean
View file

@ -47,10 +47,10 @@ structure axiom_val extends declaration_val :=
We need this feature to be able to load their values on demand in the kernel. -/
structure definition_val extends declaration_val :=
(value : expr) (hints : reducibility_hints) (is_meta : bool)
(value : task expr) (hints : reducibility_hints) (is_meta : bool)
structure theorem_val extends declaration_val :=
(value : expr)
(value : task expr)
structure constructor :=
(id : name) (type : expr)
@ -149,8 +149,8 @@ def type (d : constant_info) : expr :=
d.to_declaration_val.type
def value : constant_info → option expr
| (defn_info {value := r, ..}) := some r
| (thm_info {value := r, ..}) := some r
| (defn_info {value := r, ..}) := some r.get
| (thm_info {value := r, ..}) := some r.get
| _ := none
def hints : constant_info → reducibility_hints