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

chore: prepare to rename "predicate-like" classes

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-10 09:53:20 -08:00
parent e4f53fd92d
commit 2ef9199c56
4 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Compiler/ConstFolding.lean
View file

@ -96,10 +96,10 @@ def mkNatEq (a b : Expr) : Expr :=
mkAppN (mkConst `Eq [levelOne]) #[(mkConst `Nat), a, b]
def mkNatLt (a b : Expr) : Expr :=
mkAppN (mkConst `Less.Less [levelZero]) #[mkConst `Nat, mkConst `Nat.less, a, b]
mkAppN (mkConst `HasLess.Less [levelZero]) #[mkConst `Nat, mkConst `Nat.less, a, b]
def mkNatLe (a b : Expr) : Expr :=
mkAppN (mkConst `LessEq.LessEq [levelZero]) #[mkConst `Nat, mkConst `Nat.lessEq, a, b]
mkAppN (mkConst `HasLessEq.LessEq [levelZero]) #[mkConst `Nat, mkConst `Nat.lessEq, a, b]
def toDecidableExpr (beforeErasure : Bool) (pred : Expr) (r : Bool) : Expr :=
match beforeErasure, r with

6
src/Lean/Delaborator.lean
View file

@ -709,16 +709,16 @@ def delabPrefixOp (op : Bool → Syntax → Delab) : Delab := whenPPOption getPP
@[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.LessEq.LessEq] def delabLE : Delab := delabInfixOp fun b x y => cond b `($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.Less.Less] def delabLT : Delab := delabInfixOp fun _ 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.Equiv.Equiv] def delabEquiv : Delab := delabInfixOp fun _ 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)

6
src/Lean/Elab/BuiltinNotation.lean
View file

@ -207,16 +207,16 @@ def expandPrefixOp (op : Name) : Macro := fun stx => do
@[builtinMacro Lean.Parser.Term.modN] def expandModN : Macro := expandInfixOp `ModN.modn
@[builtinMacro Lean.Parser.Term.pow] def expandPow : Macro := expandInfixOp `Pow.pow
@[builtinMacro Lean.Parser.Term.le] def expandLE : Macro := expandInfixOp `LessEq.LessEq
@[builtinMacro Lean.Parser.Term.le] def expandLE : Macro := expandInfixOp `HasLessEq.LessEq
@[builtinMacro Lean.Parser.Term.ge] def expandGE : Macro := expandInfixOp `GreaterEq
@[builtinMacro Lean.Parser.Term.lt] def expandLT : Macro := expandInfixOp `Less.Less
@[builtinMacro Lean.Parser.Term.lt] def expandLT : Macro := expandInfixOp `HasLess.Less
@[builtinMacro Lean.Parser.Term.gt] def expandGT : Macro := expandInfixOp `Greater
@[builtinMacro Lean.Parser.Term.eq] def expandEq : Macro := expandInfixOp `Eq
@[builtinMacro Lean.Parser.Term.ne] def expandNe : Macro := expandInfixOp `Ne
@[builtinMacro Lean.Parser.Term.beq] def expandBEq : Macro := expandInfixOp `BEq.beq
@[builtinMacro Lean.Parser.Term.bne] def expandBNe : Macro := expandInfixOp `bne
@[builtinMacro Lean.Parser.Term.heq] def expandHEq : Macro := expandInfixOp `HEq
@[builtinMacro Lean.Parser.Term.equiv] def expandEquiv : Macro := expandInfixOp `Equiv.Equiv
@[builtinMacro Lean.Parser.Term.equiv] def expandEquiv : Macro := expandInfixOp `HasEquiv.Equiv
@[builtinMacro Lean.Parser.Term.and] def expandAnd : Macro := expandInfixOp `And
@[builtinMacro Lean.Parser.Term.or] def expandOr : Macro := expandInfixOp `Or

4
src/Lean/Meta/AppBuilder.lean
View file

@ -410,11 +410,11 @@ def mkDecideProof (p : Expr) : m Expr := liftMetaM do
/-- Return `a < b` -/
def mkLt (a b : Expr) : m Expr :=
mkAppM `Less.Less #[a, b]
mkAppM `HasLess.Less #[a, b]
/-- Return `a <= b` -/
def mkLe (a b : Expr) : m Expr :=
mkAppM `LessEq.LessEq #[a, b]
mkAppM `HasLessEq.LessEq #[a, b]
/-- Return `arbitrary α` -/
def mkArbitrary (α : Expr) : m Expr :=