Skip to content

Commit

Permalink
chore: Remove the ToExpr Int instance (#58)
Browse files Browse the repository at this point in the history
This instance now exists both upstream in core and downstream in mathlib (see [Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Lean.2EToExpr.20Int/near/474914783)).

The one upstream uses `toExpr (-1) = q(-1)`, which is probably preferable to the `toExpr (-1) = q(Int.negSucc 0)` used here.
  • Loading branch information
eric-wieser authored Oct 5, 2024
1 parent 2c8ae45 commit 2b2f6d7
Showing 1 changed file with 0 additions and 6 deletions.
6 changes: 0 additions & 6 deletions Qq/ForLean/ToExpr.lean
Original file line number Diff line number Diff line change
Expand Up @@ -2,12 +2,6 @@ import Lean

open Lean

instance : ToExpr Int where
toTypeExpr := .const ``Int []
toExpr i := match i with
| .ofNat n => mkApp (.const ``Int.ofNat []) (toExpr n)
| .negSucc n => mkApp (.const ``Int.negSucc []) (toExpr n)

instance : ToExpr MVarId where
toTypeExpr := .const ``MVarId []
toExpr i := mkApp (.const ``MVarId.mk []) (toExpr i.name)
Expand Down

0 comments on commit 2b2f6d7

Please sign in to comment.