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

test: deriving DecidableEq for enum types

Browse source 
Forgot to add test.
This commit is contained in:
Leonardo de Moura 2021-09-09 17:47:23 -07:00
parent 5154f462f8
commit 7607a24469
1 changed files with 29 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
tests/lean/run/enumDecEq.lean Normal file
View file

@ -0,0 +1,29 @@
inductive Foo1 where
| a1
deriving DecidableEq
#print Foo1.ofNat
inductive Foo2 where
| a1 | a2
deriving DecidableEq
#print Foo2.ofNat
inductive Foo3 where
| a1 | a2 | a3
deriving DecidableEq
#print Foo3.ofNat
inductive Foo4 where
| a1 | a2 | a3 | a4
deriving DecidableEq
#print Foo4.ofNat
inductive Foo5 where
| a1 | a2 | a3 | a4 | a5
deriving DecidableEq
#print Foo5.ofNat