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

test: remove workaround

Browse source
This commit is contained in:
Leonardo de Moura 2022-03-06 13:58:42 -08:00
parent 46d1111d3d
commit 10bccfe501
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/run/interp.lean
View file

@ -2,7 +2,7 @@ inductive Vector (α : Type u) : Nat → Type u
| nil : Vector α 0
| cons : α → Vector α n → Vector α (n+1)
infix:67 (priority := high) " :: " => Vector.cons
infix:67 " :: " => Vector.cons
inductive Ty where
| int