From 0d4da4bc7635bd434af68f9e332f601e8ec69710 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 7 Mar 2019 10:14:15 -0800 Subject: [PATCH] fix(library/init/lean/elaborator): borrow annotations @kha I see you found this problem too :) --- library/init/lean/elaborator.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean index 4a316f0a94..1d6eacd326 100644 --- a/library/init/lean/elaborator.lean +++ b/library/init/lean/elaborator.lean @@ -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