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

test(tests/lean/run/term_app): add test for nested inductive type

Browse source
This commit is contained in:
Leonardo de Moura 2017-05-24 13:36:58 -07:00
parent 1d7dd20091
commit e3249dfdb9
1 changed files with 14 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
tests/lean/run/term_app.lean Normal file
View file

@ -0,0 +1,14 @@
inductive term
| const : string → term
| app : string → list term → term
/- TODO(Leo): remove after we fix bug in lemma generator. -/
set_option eqn_compiler.lemmas false
mutual def num_consts, num_consts_lst
with num_consts : term → nat
| (term.const n) := 1
| (term.app n ts) := num_consts_lst ts
with num_consts_lst : list term → nat
| [] := 0
| (t::ts) := num_consts t + num_consts_lst ts