Collecting free variables

Stream: lean4

[Patrick Massot]

Given e : Expr, I can get a list of free variables that appear in e using (← e.collectFVars.run {}).2.fvarSet.toList. But the ordering of this list seems completely random, and even seems to varies depending on surrounding code. Is there a variant of this that is closer to list the free variables in the order where they show up in the expression? I’m aware that this order depends on notations, but in my use cases there is no complicated case.

[Henrik Böving]

You can query the fvarIds instead of the fvarSet of the resulting State object and should get a more consistent order I think. But why exactly do you want to rely on the ordering?

[Patrick Massot]

Thanks!