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

chore(tests/lean/run/measurable): remove obsolete test

Browse source
This commit is contained in:
Leonardo de Moura 2016-07-23 19:05:09 -07:00
parent 461b5f289c
commit 9ca065e7ee
1 changed files with 0 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
tests/lean/run/measurable.lean
View file

@ -1,7 +0,0 @@
open prod nat
example (a b : nat) : size_of (a, true, tt, (λ c d : nat, c + d), option.some b) = a + b :=
rfl
example : size_of (pair (pair (pair (2:nat) true) (λ a : nat, a)) (option.some (3:nat))) = 5 :=
rfl