Nat.succ of a nat literal

Stream: lean4

[Heather Macbeth]

Is it possible to write a theorem foo such that foo 37 a is syntactically 38 ≤ a ∨ a ≤ 37? (For all values of 37.). I tried

theorem foo (a b : Nat) : OfNat.ofNat a.succ ≤ b ∨ b ≤ OfNat.ofNat a := Nat.lt_or_ge a b

but although this is the result I wanted up to defeq, it isn't actually the result I wanted.

example (a : Nat) : True := by
  have := foo 37 a -- infoview shows `OfNat.ofNat (Nat.succ 37) ≤ a ∨ a ≤ OfNat.ofNat 37`
  have := foo (nat_lit 37) a -- infoview shows `OfNat.ofNat (Nat.succ 37) ≤ a ∨ a ≤ 37`
  sorry

[Heather Macbeth]

Also, same question but for (a : Nat) (b : Int),

[James Gallicchio]

is it allowed to be a custom macro that just looks like a theorem? :joy:

[Heather Macbeth]

Sure, do tell! :)

[Mario Carneiro]

import Lean

macro "foo" n:num a:term:arg : term =>
  `(show $(Lean.quote (n.getNat+1)) ≤ $a ∨ $a ≤ $n from Nat.lt_or_ge ..)

example (a : Nat) : True := by
  have := foo 37 a -- infoview shows `this: 38 ≤ a ∨ a ≤ 37`
  sorry

[Heather Macbeth]

That's pretty cool. Thanks!