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

fix(library/init/lean/compiler/ir/compilerm): borrow annotations on extern decls do not do anything right now

Browse source
This commit is contained in:
Sebastian Ullrich 2019-09-08 13:33:51 +02:00
parent 3ee59aa17f
commit 560e7af128
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/lean/compiler/ir/compilerm.lean
View file

@ -92,7 +92,7 @@ registerSimplePersistentEnvExtension {
constant declMapExt : SimplePersistentEnvExtension Decl DeclMap := default _
@[export lean_ir_find_env_decl]
def findEnvDecl (env : @& Environment) (n : @& Name) : Option Decl :=
def findEnvDecl (env : Environment) (n : Name) : Option Decl :=
(declMapExt.getState env).find n
def findDecl (n : Name) : CompilerM (Option Decl) :=