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

fix: test

Browse source
This commit is contained in:
E.W.Ayers 2022-06-03 19:54:32 -04:00 • committed by Leonardo de Moura
parent 8311c88fd0
commit c8fc371eb9
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/PPRoundtrip.lean
View file

@ -58,7 +58,7 @@ section
#eval checkM `(id Nat)
#eval checkM `(Sum Nat Nat)
end
#eval checkM `(id (id Nat)) (Std.RBMap.empty.insert (SubExpr.Pos.encode #[1]) $ KVMap.empty.insert `pp.explicit true)
#eval checkM `(id (id Nat)) (Std.RBMap.empty.insert (SubExpr.Pos.ofArray #[1]) $ KVMap.empty.insert `pp.explicit true)
-- specify the expected type of `a` in a way that is not erased by the delaborator
def typeAs.{u} (α : Type u) (a : α) := ()