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

chore: remove temporary workaround

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-14 10:08:29 -08:00
parent 0b58ebfba2
commit f24fff7985
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/PrettyPrinter/Delaborator/Builtins.lean
View file

@ -219,7 +219,7 @@ def delabAppMatch : Delab := whenPPOption getPPNotation do
Syntax.mkApp stx st.moreArgs
| _, #[] => failure
| _, _ =>
let discrs ← st.discrs.mapM fun discr => `(Parser.Term.matchDiscr|$discr:term)
let discrs ← st.discrs.mapM fun discr => `(matchDiscr|$discr:term)
let pats ← delabPatterns st
let stx ← `(match $[$discrs],* with | $[$[$pats],* => $st.rhss]|*)
Syntax.mkApp stx st.moreArgs