Zulip Chat Archive

Stream: general

Topic: tactic noobie


view this post on Zulip Johan Commelin (Sep 14 2018 at 11:54):

I'm taking a stab at the tfae tactic. This is what I have so far:

meta def tfae_have
  (p₁ : parse small_nat)
  (re : parse (((tk "→" <|> tk "->") *> return tt) <|> ((tk "↔" <|> tk "<->") *> return ff)))
  (p₂ : parse small_nat)
  (discharger : tactic unit :=
    (solve_by_elim <|> tauto <|> using_smt (smt_tactic.intros >> smt_tactic.solve_goals))) :
  tactic unit := do
    g <- get_goals,

Now I would like to loop over my goals, and check if any of them has the form tfae [P, Q, ..., bla]. How do I do that?

view this post on Zulip Reid Barton (Sep 14 2018 at 11:59):

maybe we can cocalc this?

view this post on Zulip Johan Commelin (Sep 14 2018 at 11:59):

Sure!

view this post on Zulip Johan Commelin (Sep 14 2018 at 11:59):

Just in the big project?

view this post on Zulip Reid Barton (Sep 14 2018 at 12:00):

Seems easiest

view this post on Zulip Johan Commelin (Sep 14 2018 at 12:00):

I'm there

view this post on Zulip Reid Barton (Sep 14 2018 at 12:03):

Maybe working on the main goal (target) is good enough. I'm looking at the split_ifs code and that is what it does

view this post on Zulip Reid Barton (Sep 14 2018 at 12:05):

I think this is going to need the tfae stuff to be defined already


Last updated: May 14 2021 at 00:42 UTC