Zulip Chat Archive

Stream: general

Topic: resolving a name


view this post on Zulip 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?)

view this post on Zulip Mario Carneiro (Sep 11 2018 at 07:30):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Sep 11 2018 at 07:36):

eval_expr is what you want

view this post on Zulip 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?

view this post on Zulip Keeley Hoek (Sep 11 2018 at 07:44):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Sep 11 2018 at 07:45):

mk_const will turn a name into an expr

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Keeley Hoek (Sep 11 2018 at 10:23):

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

view this post on Zulip Kenny Lau (Sep 11 2018 at 10:25):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 11 2018 at 10:49):

Well, even "this section only"

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Keeley Hoek (Sep 11 2018 at 13:13):

It seems that tactic.unset_attribute does perform the unsetting... Perhaps this is a bug in lean?

view this post on Zulip Sebastian Ullrich (Sep 11 2018 at 17:14):

@Keeley Hoek "Unsetting" an attribute means using attribute [-simp] ..., not just leaving the scope of a local attribute declaration

view this post on Zulip Keeley Hoek (Sep 11 2018 at 17:15):

fair enough!

view this post on Zulip Edward Ayers (Sep 17 2018 at 09:17):

Hi I've been on hols.

view this post on Zulip Patrick Massot (Sep 17 2018 at 09:18):

Welcome back!

view this post on Zulip Kevin Buzzard (Sep 17 2018 at 09:18):

We thought you were dead!

view this post on Zulip Kevin Buzzard (Sep 17 2018 at 09:18):

We were worried

view this post on Zulip Patrick Massot (Sep 17 2018 at 09:18):

Or worse than dead: decided to use another proof assistant

view this post on Zulip Edward Ayers (Sep 17 2018 at 09:18):

I was flirting with Isabelle again a bit

view this post on Zulip Johan Commelin (Sep 17 2018 at 09:20):

Lol, I knew that :thumbs_up: was coming...

view this post on Zulip Johannes Hölzl (Sep 17 2018 at 09:20):

hehe

view this post on Zulip Patrick Massot (Sep 17 2018 at 09:20):

Scott, did we understand correctly what you learned in Dagstuhl?


Last updated: May 10 2021 at 00:31 UTC