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

fix: remove redundant alternatives

Browse source
This commit is contained in:
Leonardo de Moura 2022-07-31 05:27:37 -07:00
parent 30efb589a6
commit feb71271e9
2 changed files with 1 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/NotationExtra.lean
View file

@ -92,11 +92,9 @@ syntax (name := calcTactic) "calc" ppLine withPosition(calcStep) ppLine withPosi
@[appUnexpander Unit.unit] def unexpandUnit : Lean.PrettyPrinter.Unexpander
| `($(_)) => `(())
| _ => throw ()
@[appUnexpander List.nil] def unexpandListNil : Lean.PrettyPrinter.Unexpander
| `($(_)) => `([])
| _ => throw ()
@[appUnexpander List.cons] def unexpandListCons : Lean.PrettyPrinter.Unexpander
| `($(_) $x []) => `([$x])

3
src/Lean/Elab/Quotation/Precheck.lean
View file

@ -112,9 +112,8 @@ private def isSectionVariable (e : Expr) : TermElabM Bool := do
for arg in args.raw do
match arg with
| `(argument| ($_ := $e)) => precheck e
| `(argument| $e:term) => precheck e
| `(argument| ..) => pure ()
| _ => throwUnsupportedSyntax
| `(argument| $e:term) => precheck e
| _ => throwUnsupportedSyntax
@[builtinQuotPrecheck Lean.Parser.Term.paren] def precheckParen : Precheck