From 29f0a1c4c91cccb198ce37e558f1e751a220089b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 8 Feb 2020 11:16:45 -0800 Subject: [PATCH] chore: nary subst --- src/Init/Lean/Parser/Term.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Lean/Parser/Term.lean b/src/Init/Lean/Parser/Term.lean index 5738e12bb6..515e7267f5 100644 --- a/src/Init/Lean/Parser/Term.lean +++ b/src/Init/Lean/Parser/Term.lean @@ -162,7 +162,7 @@ def checkIsSort := checkStackTop (fun stx => stx.isOfKind `Lean.Parser.Term.type @[builtinTermParser] def heq := tparser! unicodeInfixL " ≅ " " ~= " 50 @[builtinTermParser] def equiv := tparser! infixL " ≈ " 50 -@[builtinTermParser] def subst := tparser! infixR " ▸ " 75 +@[builtinTermParser] def subst := tparser! symbol " ▸ " 75 >> sepBy1 (termParser 75) " ▸ " @[builtinTermParser] def and := tparser! unicodeInfixR " ∧ " " /\\ " 35 @[builtinTermParser] def or := tparser! unicodeInfixR " ∨ " " \\/ " 30