Meta: Check whether we have a concrete number

Stream: Is there code for X?

[Max Nowak 🐉]

I am writing a simproc, and want to simplify something of form f n, but only when n is a concrete number (in my case, Fin N). I recall there being some convenience functions for checking that, but what were they called?

[Edward van de Meent]

i don't know about simprocs, but...
@loogle "isNatLit"

[loogle]

:search: Lean.Syntax.isNatLit?

[Edward van de Meent]

@loogle "NatLit"

[loogle]

:search: rawNatLit, Lean.Syntax.decodeNatLitVal?, and 17 more

[Max Nowak 🐉]

@loogle "isFinLit"

[loogle]

:shrug: nothing found

[Henrik Böving]

isNatLit? works on Syntax, thats not what you are looking for in a simproc, what you want is a function that can parse an Expr, for Fin we commonly use docs#Lean.Meta.getFinValue?

[Max Nowak 🐉]

getFinValue? on the following expression returns none:

@Fin.mk (@OfNat.ofNat.{0} Nat 16 (instOfNatNat 16)) (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))
  (@Nat.le_of_ble_eq_true (Nat.succ (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)))
    (@OfNat.ofNat.{0} Nat 16 (instOfNatNat 16)) (@rfl.{1} Bool Bool.true))

[Henrik Böving]

Sure, after all the doc string says it's looking for OfNat.ofNat applications for Fin. I think for this case we might want to consider adding suppport for more means to create a Fin, e.g. like with getBitVecValue?, feel free to open an issue about it.

[Henrik Böving]

I guess we could generally consider extending more literal functions to account for more ways to denote literals, not quite sure what the reason that they are as limited as they are currently is.