How to make a term of `OfNat.ofNat i : Fin (n + 1)` legally?

Stream: metaprogramming / tactics

[Dexin Zhang]

I wrote the following code:

open Lean in
/-- Create an expression of `OfNat.ofNat i : Fin (n + 1)`. -/
def mkOfNat (i : ℕ) (n : Expr) : Expr :=
  mkApp3 (.const ``OfNat.ofNat [0]) (mkApp (.const ``Fin []) (mkNatAdd n (mkNatLit 1))) (mkNatLit i)
    (mkApp3 (.const ``Fin.instOfNat []) (mkNatAdd n (mkNatLit 1))
      (mkApp (.const ``Nat.instNeZeroSucc []) n) (mkNatLit i))

open Lean Meta in
#eval do
  let e := mkOfNat 1 (mkNatLit 3)
  logInfo m!"{e}" -- OfNat.ofNat 1
  logInfo m!"{← getOfNatValue? e ``Fin}" -- none

It does create e as OfNat.ofNat 1 : Fin 3, but the pretty printer shows it as OfNat.ofNat 1, not 1. Also, when I try to use getOfNatValue? to extract the value of e, it fails.

[Aaron Liu]

mkRawNatLit

[Henrik Böving]

When you try to imitate terms built by the elaborator I would suggest simply looking at what the elaborator did:

variable (n : Nat)

set_option pp.explicit true in
#check (1 : Fin (n + 1))

[Dexin Zhang]

Aaron Liu said:

mkRawNatLit

Thanks, it really works!

[Dexin Zhang]

Henrik Böving said:

When you try to imitate terms built by the elaborator I would suggest simply looking at what the elaborator did:

variable (n : Nat)

set_option pp.explicit true in
#check (1 : Fin (n + 1))

Thanks, I did try this before, but I don't know what causes the difference then (which turns out to be mkNatLit and mkRawNatLit).