print list name

Stream: general

[Johan Commelin]

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.)

[Johan Commelin]

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 (-;

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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?

[Johan Commelin]

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

[Johan Commelin]

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.

[Johan Commelin]

Because monads are just cool mathematical goodies.

[Johan Commelin]

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)

[Johan Commelin]

That seems to do what I want (-;

[Kevin Buzzard]

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.

[Mario Carneiro]

here's another way:

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

[Mario Carneiro]

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

[Johan Commelin]

Right! That's nice (-;

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Johan Commelin]

Right. That makes sense.