reflection

Stream: general

[Sarah Mameche]

Hi,
I'm trying to map meta expressions to an inductive type in the object language (with pattern matching on expr as described in https://leanprover.github.io/papers/tactic.pdf).
There's a constructor taking a natural number as argument (var : ℕ → term). How can the number be extracted from an expression with this constructor?
Also, how does this work if I go from the inductive type back to exprs?

[Rob Lewis]

I'm not sure if I understand exactly what you're after. You want a function expr → ℕ that will return the index if the input is made with expr.var?

meta def var_index : expr → ℕ
| (expr.var n) := n
| _ := 0

You can do the same in the other direction, if the nat appears in a constructor of your inductive type. Match on your type, get the nat argument, and feed it back into expr.var.

[Rob Lewis]

Or did you mean something else?

[Sarah Mameche]

No, that helped, thanks!