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

fix(library/init/lean/elaborator): borrow annotations

Browse source 
@kha I see you found this problem too :)
This commit is contained in:
Leonardo de Moura 2019-03-07 10:14:15 -08:00
parent b5b2adea49
commit 0d4da4bc76
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/lean/elaborator.lean
View file

@ -17,7 +17,7 @@ constant environment : Type
@[extern "lean_environment_mk_empty"]
constant environment.mk_empty : unit → environment
@[extern "lean_environment_contains"]
constant environment.contains : @& environment → @& name → bool
constant environment.contains : (@& environment) → (@& name) → bool
-- deprecated constructor
@[extern "lean_expr_local"]
constant expr.local : name → name → expr → binder_info → expr
@ -46,7 +46,7 @@ structure old_elaborator_state :=
(ns : name)
@[extern "lean_elaborator_elaborate_command"]
constant elaborate_command (filename : @& string) : expr → @& old_elaborator_state →
constant elaborate_command (filename : @& string) : expr → (@& old_elaborator_state) →
option old_elaborator_state × message_log
open parser