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

chore: remove obsolete builtin delaborators

Browse source
This commit is contained in:
Sebastian Ullrich 2020-11-30 16:56:09 +01:00 • committed by Leonardo de Moura
parent d18596d4ca
commit 07f25a19db
1 changed files with 0 additions and 63 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -472,69 +472,6 @@ def delabCoe : Delab := whenPPOption getPPCoercions do
@[builtinDelab app.coeFun]
def delabCoeFun : Delab := delabCoe
def delabInfixOp (op : Bool → Syntax → Syntax → Delab) : Delab := whenPPOption getPPNotation do
let stx ← delabAppImplicit <|> delabAppExplicit
guard $ stx.isOfKind `Lean.Parser.Term.app && (stx.getArg 1).getNumArgs == 2
let unicode ← getPPOption getPPUnicode
let args := stx.getArg 1
op unicode (args.getArg 0) (args.getArg 1)
def delabPrefixOp (op : Bool → Syntax → Delab) : Delab := whenPPOption getPPNotation do
let stx ← delabAppImplicit <|> delabAppExplicit
guard $ stx.isOfKind `Lean.Parser.Term.app && (stx.getArg 1).getNumArgs == 1
let unicode ← getPPOption getPPUnicode
let args := stx.getArg 1
op unicode (args.getArg 0)
@[builtinDelab app.Prod] def delabProd : Delab := delabInfixOp fun _ x y => `($x × $y)
@[builtinDelab app.Function.comp] def delabFComp : Delab := delabInfixOp fun _ x y => `($x ∘ $y)
@[builtinDelab app.Add.add] def delabAdd : Delab := delabInfixOp fun _ x y => `($x + $y)
@[builtinDelab app.Sub.sub] def delabSub : Delab := delabInfixOp fun _ x y => `($x - $y)
@[builtinDelab app.Mul.mul] def delabMul : Delab := delabInfixOp fun _ x y => `($x * $y)
@[builtinDelab app.Div.div] def delabDiv : Delab := delabInfixOp fun _ x y => `($x / $y)
@[builtinDelab app.Mod.mod] def delabMod : Delab := delabInfixOp fun _ x y => `($x % $y)
@[builtinDelab app.ModN.modn] def delabModN : Delab := delabInfixOp fun _ x y => `($x %ₙ $y)
@[builtinDelab app.Pow.pow] def delabPow : Delab := delabInfixOp fun _ x y => `($x ^ $y)
@[builtinDelab app.HasLessEq.LessEq] def delabLE : Delab := delabInfixOp fun b x y => cond b `($x ≤ $y) `($x <= $y)
@[builtinDelab app.GreaterEq] def delabGE : Delab := delabInfixOp fun b x y => cond b `($x ≥ $y) `($x >= $y)
@[builtinDelab app.HasLess.Less] def delabLT : Delab := delabInfixOp fun _ x y => `($x < $y)
@[builtinDelab app.Greater] def delabGT : Delab := delabInfixOp fun _ x y => `($x > $y)
@[builtinDelab app.Eq] def delabEq : Delab := delabInfixOp fun _ x y => `($x = $y)
@[builtinDelab app.Ne] def delabNe : Delab := delabInfixOp fun _ x y => `($x ≠ $y)
@[builtinDelab app.BEq.beq] def delabBEq : Delab := delabInfixOp fun _ x y => `($x == $y)
@[builtinDelab app.bne] def delabBNe : Delab := delabInfixOp fun _ x y => `($x != $y)
@[builtinDelab app.HEq] def delabHEq : Delab := delabInfixOp fun b x y => cond b `($x ≅ $y) `($x ~= $y)
@[builtinDelab app.HasEquiv.Equiv] def delabEquiv : Delab := delabInfixOp fun _ x y => `($x ≈ $y)
@[builtinDelab app.And] def delabAnd : Delab := delabInfixOp fun b x y => cond b `($x ∧ $y) `($x /\ $y)
@[builtinDelab app.Or] def delabOr : Delab := delabInfixOp fun b x y => cond b `($x ∨ $y) `($x || $y)
@[builtinDelab app.Iff] def delabIff : Delab := delabInfixOp fun b x y => cond b `($x ↔ $y) `($x <-> $y)
@[builtinDelab app.and] def delabBAnd : Delab := delabInfixOp fun _ x y => `($x && $y)
@[builtinDelab app.or] def delabBOr : Delab := delabInfixOp fun _ x y => `($x || $y)
@[builtinDelab app.Append.append] def delabAppend : Delab := delabInfixOp fun _ x y => `($x ++ $y)
@[builtinDelab app.List.cons] def delabCons : Delab := delabInfixOp fun _ x y => `($x :: $y)
@[builtinDelab app.AndThen.andthen] def delabAndThen : Delab := delabInfixOp fun _ x y => `($x >> $y)
@[builtinDelab app.Bind.bind] def delabBind : Delab := delabInfixOp fun _ x y => `($x >>= $y)
@[builtinDelab app.Seq.seq] def delabseq : Delab := delabInfixOp fun _ x y => `($x <*> $y)
@[builtinDelab app.SeqLeft.seqLeft] def delabseqLeft : Delab := delabInfixOp fun _ x y => `($x <* $y)
@[builtinDelab app.SeqRight.seqRight] def delabseqRight : Delab := delabInfixOp fun _ x y => `($x *> $y)
@[builtinDelab app.Functor.map] def delabMap : Delab := delabInfixOp fun _ x y => `($x <$> $y)
@[builtinDelab app.Functor.mapRev] def delabMapRev : Delab := delabInfixOp fun _ x y => `($x <&> $y)
@[builtinDelab app.OrElse.orelse] def delabOrElse : Delab := delabInfixOp fun _ x y => `($x <|> $y)
@[builtinDelab app.orM] def delabOrM : Delab := delabInfixOp fun _ x y => `($x <||> $y)
@[builtinDelab app.andM] def delabAndM : Delab := delabInfixOp fun _ x y => `($x <&&> $y)
@[builtinDelab app.Not] def delabNot : Delab := delabPrefixOp fun _ x => `(¬ $x)
@[builtinDelab app.not] def delabBNot : Delab := delabPrefixOp fun _ x => `(! $x)
@[builtinDelab app.List.nil]
def delabNil : Delab := whenPPOption getPPNotation do
guard $ (← getExpr).getAppNumArgs == 1