From c8fc371eb98bd9842e36b157d55ba2987dac04d7 Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Fri, 3 Jun 2022 19:54:32 -0400 Subject: [PATCH] fix: test --- tests/lean/PPRoundtrip.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/PPRoundtrip.lean b/tests/lean/PPRoundtrip.lean index 221f412a59..81e1d98089 100644 --- a/tests/lean/PPRoundtrip.lean +++ b/tests/lean/PPRoundtrip.lean @@ -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 : α) := ()