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

chore: fix test

Browse source
This commit is contained in:
Sebastian Ullrich 2022-06-04 17:24:33 +02:00 • committed by Leonardo de Moura
parent f9e2a65f75
commit 130cc8bbd5
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/lean/rwEqThms.lean.expected.out
View file

@ -2,9 +2,9 @@
a : α
as bs : List α
h : bs = a :: as
⊢ List.length (?a :: as) = List.length bs
⊢ List.length (?head :: as) = List.length bs
case a
case head
α : Type ?u
a : α
as bs : List α