Zulip Chat Archive

Stream: new members

Topic: given expression should not contain de-Bruijn variables


view this post on Zulip Lucas Allen (Aug 25 2020 at 06:21):

G'day. I have the following meta code

meta def recurse_pi : expr  tactic unit
| (expr.pi _ _ v b) := do t  infer_type v,
                          trace t,
                          recurse_pi b
| _ := skip

#eval recurse_pi `( {a b : Prop}, (a  b)  (b  a)  (a  b))

I want this to print out

Type
Type
Prop
Prop

But it prints out

Type
Type

and gives the error "tactic 'infer_type' failed, given expression should not contain de-Bruijn variables, they should be replaced with local constants before using this tactic"

How do I replace de-Bruijn variables with local constants? And/or is there a better way to do what I want? Thanks.


Last updated: May 09 2021 at 20:11 UTC