Zulip Chat Archive

Stream: general

Topic: resolving a name

Keeley Hoek (Sep 11 2018 at 07:24):

Say I've got n : name, which I get passed, but would like to be of type my_type. I know I can use t <- infer_type n to get the type of the identifier pointed to by n, and then can use an if to guard against the type being wrong. But I'd really like to do more and "cast" n to type my_type, getting some inst : my_type from n. Would anyone be able to point me to a nice/any facility for doing this? (I've grepped for cast without success, is mk_app what I'm looking for?)

Mario Carneiro (Sep 11 2018 at 07:30):

I don't quite understand the setup here. How does my_type relate to n?

Keeley Hoek (Sep 11 2018 at 07:35):

Sorry: secretly in some file a user wrote def foo : my_type := blah, and then in tactic mode later on they called my code cast_fn `(foo) . So here n = `foo, and I'd like cast_fn to be of type name -> tactic my_type.

Keeley Hoek (Sep 11 2018 at 07:36):

Maybe my attempt at an MWE confused the issue. I'm getting a name in an attribute handler, and I expect what was annotated to be of a particular type. I'd like to get the actual thing that was annotated and call a function on it.

Mario Carneiro (Sep 11 2018 at 07:36):

eval_expr is what you want

Keeley Hoek (Sep 11 2018 at 07:38):

Right. So to invoke it, I only get to pass a single expr, so I figure I need to convert the name of the function I want to call into an expr and then create a expr which says "evaluate the function at the first expr". How can I build such an expr?

Keeley Hoek (Sep 11 2018 at 07:44):

Ah. I think eval_expr my_type (expr.app `(my_fn) n) does the job!

Keeley Hoek (Sep 11 2018 at 07:45):

Ok, so the point of mk_app is that I don't need to know the type beforehand? Right.

Mario Carneiro (Sep 11 2018 at 07:45):

mk_const will turn a name into an expr

Kevin Buzzard (Sep 11 2018 at 07:48):

This whole area is just screaming out for a small pdf or web page containing 10 very basic examples followed by 10 very basic questions.

Patrick Massot (Sep 11 2018 at 07:50):

What happened to @Edward Ayers? He started to write such documentation and then vanished? Is there a meta-documentation curse?

Keeley Hoek (Sep 11 2018 at 10:23):

What does the local in local attribute ... mean?

Kenny Lau (Sep 11 2018 at 10:25):

https://en.wikipedia.org/wiki/Scope_(computer_science)

Kevin Buzzard (Sep 11 2018 at 10:31):

I think it means "it's an attribute for this .lean file only" in this case, but I'm certainly not an expert.

Johan Commelin (Sep 11 2018 at 10:49):

Well, even "this section only"

Keeley Hoek (Sep 11 2018 at 13:05):

Haha thanks Kenny, I've written a fair few curly-braces in my time!

In that case does anyone know if the before_unset member of user_attribute is ever actually called when a local attribute is removed for the reason that a section has ended? It seems that it is not, which I find very strange.

Keeley Hoek (Sep 11 2018 at 13:09):

It seems that the none of mathlib and only one file in the lean library itself uses the feature, and this is in library/init/meta/smt/ematch.lean where before_unset is defined to do nothing anyway.