search

leanprover-community / quote4

Intuitive, type-safe expression quotations for Lean 4.
Apache License 2.0
75 stars 12 forks source link

fix: correct matching on sigma types #26

Closed eric-wieser closed 11 months ago

gebner commented 11 months ago

Oh wow, this must've been broken since the removal of the implicit pure coercion... Thank you so much for fixing this!

eric-wieser commented 11 months ago

It would be cool if

/-- Given `x + y` of Nat, returns `(x, y)`. Otherwise fail. -/
def getNatAdd (e : Expr) : MetaM (Option (Q(Nat) × Q(Nat))) := do
  let ⟨_, ~q(Nat), ~q($a + $b)⟩ ← inferTypeQ e | return none
  return some (a, b)

worked, but that would need a more cooperative elaboration order