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

chore: use new_frontend in the whole test

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-21 09:14:55 -08:00
parent 35383bf862
commit 2b63aa27d3
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/lean/run/macro.lean
View file

@ -1,11 +1,11 @@
new_frontend
abbrev Set (α : Type) := α → Prop
axiom setOf {α : Type} : (α → Prop) → Set α
axiom mem {α : Type} : α → Set α → Prop
axiom univ {α : Type} : Set α
axiom Union {α : Type} : Set (Set α) → Set α
new_frontend
syntax term " ∈ ":100 term:99 : term
macro_rules