Zulip Chat Archive

Stream: lean4

Topic: expr.local_const


view this post on Zulip Uranus Testing (Feb 02 2021 at 16:39):

Is there no replacement in Lean 4 for expr.local_const (https://github.com/leanprover/lean/blob/master/library/init/meta/expr.lean#L43)?

view this post on Zulip Reid Barton (Feb 02 2021 at 16:42):

It's Expr.fvar I think.

view this post on Zulip Uranus Testing (Feb 02 2021 at 16:44):

Expr.fvar does not contain any information about bindingDomain, how I see.

view this post on Zulip Mario Carneiro (Feb 02 2021 at 16:45):

free variables don't bind anything...? bindingDomain only makes sense for pi types and lambdas

view this post on Zulip Sebastian Ullrich (Feb 02 2021 at 16:48):

Yes, this has changed. Free variables now only make sense in relation to the surrounding local context, which holds the domain.

view this post on Zulip Uranus Testing (Feb 02 2021 at 16:53):

So is there a way to call Meta.inferType with some additions to the global context without modifying it?

view this post on Zulip Sebastian Ullrich (Feb 02 2021 at 16:55):

No, that's what the local context is for

view this post on Zulip Reid Barton (Feb 02 2021 at 16:56):

BTW, if you're not already aware, you'll probably find the slides posted around here useful.

view this post on Zulip Uranus Testing (Feb 02 2021 at 16:57):

Sebastian Ullrich said:

No, that's what the local context is for

OK, thanks.


Last updated: May 18 2021 at 23:14 UTC