Passing integer arguments in a tactic

Stream: metaprogramming / tactics

[Anirudh Suresh]

import Mathlib
import Lean
import Lean.Elab.Tactic
import Lean.Elab.Term
import Lean.Meta
import Quantum.Essential_math_lemmas
open Lean
open Lean.Elab.Tactic
open Lean.Elab.Term
open Lean.Meta
open scoped Matrix
open Matrix


elab "tactic_num " "("n1:term "," n2:term ") ": tactic => do
  let n1Expr ← Elab.Tactic.elabTerm n1 none
  let iVal ← match n1Expr.rawNatLit? with
    | some v => pure v
    | none   => throwError "tactic_num: first argument not a numeric literal {n1Expr}"
  -- elaborate second numeral and extract Nat
  let n2Expr ← Elab.Tactic.elabTerm n2 none
  let jVal ← match n2Expr.rawNatLit? with
    | some v => pure v
    | none   => throwError "tactic_num: second argument not a numeric literal"
  pure ()

lemma l: 1+2=3:= by {
  tactic_num (1,2)
}

I want to pass integer arguments in my tactic which I want to get as a natural number. However, I am not able to do so with the rawNatLit?. Is there any other function or any other way I can do this so that I pass in the argument and then I am able to get the value as type "Option Nat" from it?

[Damiano Testa]

Can't you use n1:num directly? I'm on mobile, so I can't test.

[Anirudh Suresh]

No that isnt working. Even if I used num, I want to get it of type

Nat

to use it later in my tactic

[Damiano Testa]

Isn't there a getNat/getNumLit or similarly named lemma?

[Damiano Testa]

docs#Lean.TSyntax.getNat, maybe?

[Damiano Testa]

So, something like this:

elab "tactic_num " "("n1:num "," n2:num ") ": tactic => do
  let n1Nat := n1.getNat
  let n2Nat := n2.getNat
  logInfo m!"The first input is {n1Nat}, the second one is {n2Nat}."

[Robin Arnez]

Anirudh Suresh schrieb:

However, I am not able to do so with the rawNatLit?.

If you want to do it with terms, then use docs#Lean.Meta.getNatValue?.

[Robin Arnez]

(or docs#Lean.Meta.getIntValue? below if that's what you want)

[Aaron Liu]

You should not be elaborating a term here, if all you want to do is to pass a number