Zulip Chat Archive

Stream: general

Topic: reflection


Sarah Mameche (Sep 25 2018 at 09:44):

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 (Sep 25 2018 at 10:05):

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 (Sep 25 2018 at 10:05):

Or did you mean something else?

Sarah Mameche (Sep 25 2018 at 12:16):

No, that helped, thanks!


Last updated: Dec 20 2023 at 11:08 UTC