summaryrefslogtreecommitdiff
path: root/testsuite/compiler/check/abstract-operations/abstract-operations.gfs
blob: aba4aaf22a74a84b2edbac5519e02de9408331b3 (plain)
1
2
3
4
5
-- here we test that the abstract operations are not used for proof search

i testsuite/compiler/check/abstract-operations/Nat.gf
gt -cat=Nat -number=10 -depth=10
pt -compute (twice (succ zero))