Zulip Chat Archive

Stream: general

Topic: print list name


view this post on Zulip Johan Commelin (Aug 09 2018 at 07:23):

My first attempt at writing a tactic. I want a tactic that will fail by printing a list of tactics. I've copy-pasted code by Scott:

meta def get_applicable_lemmas : tactic name :=
do cs  attribute.get_instances `applicable,
   fail -- <what do I put here?>

(Whoops, there was still code that tried to apply the tactics, only failing if none applied. That's now gone.)

view this post on Zulip Johan Commelin (Aug 09 2018 at 07:23):

Oh, and maybe there is a far easier way to look up all the current applicable lemmas then by writing a failing tactic. If so, I'dd also like to learn that method (-;

view this post on Zulip Mario Carneiro (Aug 09 2018 at 07:25):

I don't quite get what you are tying to do

view this post on Zulip Johan Commelin (Aug 09 2018 at 07:25):

I want Lean to print me a list of all lemmas that are tagged with applicable.

view this post on Zulip Johan Commelin (Aug 09 2018 at 07:25):

Hmmm, can I do this with #print attribute applicable or something similar?

view this post on Zulip Johan Commelin (Aug 09 2018 at 07:27):

Where do I what sorts of things I can #print anyways? So far I've learned two or three incantations by osmosis in this chat. Is this documented anywhere?

view this post on Zulip Johan Commelin (Aug 09 2018 at 07:27):

#print attribute is not a valid print command )-;

view this post on Zulip Johan Commelin (Aug 09 2018 at 07:35):

So, I need to fold \lam n, n.to_string over this list, right? And I can just use the regular fold. I don't need some meta-fold.

view this post on Zulip Johan Commelin (Aug 09 2018 at 07:35):

Because monads are just cool mathematical goodies.

view this post on Zulip Johan Commelin (Aug 09 2018 at 07:42):

meta def get_applicable_lemmas : tactic unit :=
do cs  attribute.get_instances `applicable,
   tactic.trace (list.foldl (λ s n, name.to_string n ++ ", " ++ s) "" cs)

view this post on Zulip Johan Commelin (Aug 09 2018 at 07:42):

That seems to do what I want (-;

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 08:20):

So, I need to fold \lam n, n.to_string over this list, right? And I can just use the regular fold. I don't need some meta-fold.

Whilst I'm kind-of out of my depth, I think that the fact that you can use regular fold is one thing that Lean has over Coq. I think that in Coq you have to learn one language to write proofs and then another language to write tactics.

view this post on Zulip Mario Carneiro (Aug 09 2018 at 08:29):

here's another way:

meta def get_applicable_lemmas : tactic unit :=
do cs ← attribute.get_instances `applicable,
   cs.mmap' tactic.trace

view this post on Zulip Mario Carneiro (Aug 09 2018 at 08:30):

or attribute.get_instances `applicable >>= list.mmap' tactic.trace if you want to be clever

view this post on Zulip Johan Commelin (Aug 09 2018 at 08:31):

Right! That's nice (-;

view this post on Zulip Johan Commelin (Aug 09 2018 at 08:32):

Of course I should have thought of looking for some map-like.

view this post on Zulip Mario Carneiro (Aug 09 2018 at 08:32):

here I am using a kind of "meta map" mmap

view this post on Zulip Mario Carneiro (Aug 09 2018 at 08:32):

although this is because I want to map from inside a monad

view this post on Zulip Mario Carneiro (Aug 09 2018 at 08:33):

mmap' is more of a "for each" or "scan" type function than a map - it doesn't return any output

view this post on Zulip Johan Commelin (Aug 09 2018 at 08:47):

What is the difference between tactic unit vs tactic name vs tactic string?

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 08:51):

that's like asking what the difference is between option unit and option nat and option real

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 08:52):

If you're passing information around between tactics then you might want to use tactic blah (which means "blah plus the extra option of failure"), but at the end of it all when you want to run the tactic you may as well return something of type "tactic unit" because no other tactic wants the output.

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 08:53):

The changing of the state is not an output of the tactic, that all goes on within the monad

view this post on Zulip Johan Commelin (Aug 09 2018 at 08:53):

Right. That makes sense.


Last updated: May 15 2021 at 23:13 UTC