test(tests/lean/abbrev1): add test for abbreviation command
This commit is contained in:
parent
43f849bf95
commit
f9832fb89f
2 changed files with 22 additions and 0 deletions
19
tests/lean/abbrev1.lean
Normal file
19
tests/lean/abbrev1.lean
Normal file
|
@ -0,0 +1,19 @@
|
|||
open nat
|
||||
|
||||
abbreviation foo : Π (A : Type), nat := λ a, 2 + 3
|
||||
|
||||
definition tst := foo nat
|
||||
|
||||
set_option pp.abbreviations false
|
||||
|
||||
print definition tst
|
||||
|
||||
set_option pp.abbreviations true
|
||||
|
||||
print definition tst
|
||||
|
||||
abbreviation id [parsing-only] {A : Type} (a : A) := a
|
||||
|
||||
definition tst1 := id 10
|
||||
|
||||
print definition tst1
|
3
tests/lean/abbrev1.lean.expected.out
Normal file
3
tests/lean/abbrev1.lean.expected.out
Normal file
|
@ -0,0 +1,3 @@
|
|||
(λ (a : Type₁), 2 + 3) ℕ
|
||||
foo ℕ
|
||||
(λ (A : Type₁) (a : A), a) num 10
|
Loading…
Reference in a new issue