Zulip Chat Archive
Stream: lean4
Topic: expr.local_const
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)?
Reid Barton (Feb 02 2021 at 16:42):
It's Expr.fvar I think.
Uranus Testing (Feb 02 2021 at 16:44):
Expr.fvar does not contain any information about bindingDomain, how I see.
Mario Carneiro (Feb 02 2021 at 16:45):
free variables don't bind anything...? bindingDomain only makes sense for pi types and lambdas
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.
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?
Sebastian Ullrich (Feb 02 2021 at 16:55):
No, that's what the local context is for
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.
Uranus Testing (Feb 02 2021 at 16:57):
Sebastian Ullrich said:
No, that's what the local context is for
OK, thanks.
Last updated: Dec 20 2023 at 11:08 UTC