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

chore: missing instance

Browse source
This commit is contained in:
Leonardo de Moura 2019-10-28 19:48:27 -07:00
parent 5878aa0471
commit 7ab79b8729
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/Init/Lean/MetavarContext.lean
View file

@ -16,6 +16,8 @@ structure MetavarContext :=
namespace MetavarContext
instance : Inhabited MetavarContext := ⟨{}⟩
@[export lean_mk_metavar_ctx]
def mkMetavarContext : Unit → MetavarContext :=
fun _ => {}