From 2b63aa27d3a7fbe013cc4a170ae222e69525ccfd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 21 Jan 2020 09:14:55 -0800 Subject: [PATCH] chore: use new_frontend in the whole test --- tests/lean/run/macro.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/lean/run/macro.lean b/tests/lean/run/macro.lean index c6745d8402..58610b5666 100644 --- a/tests/lean/run/macro.lean +++ b/tests/lean/run/macro.lean @@ -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