Zulip Chat Archive

Stream: general

Topic: Tactic help


Koundinya Vajjha (Jan 02 2019 at 16:54):

Hi, in order to get familiar with writing tactics, I am trying to write a simple tactic to count the number of occurrences of in a goal. Here is what I have so far:

meta def is_empty' : expr  bool
| `(has_emptyc.emptyc _) := tt
| _ := ff

meta def list_emptys' (e : expr) : list expr :=
e.fold []
(λ e' _ es, if (is_empty' e') then insert e' es else es)

meta def find_empty : tactic unit :=
do e  tactic.target,
tactic.trace $ (list_emptys' e)

But if I run this tactic

universe u
example {s : Type u} (a b : set s) :    = a :=
begin
find_empty,
end

I only get [∅]. Can someone help me figure out what I am doing wrong? I'm guessing it's me not understanding how fold works for expr...

Mario Carneiro (Jan 02 2019 at 17:23):

you used insert to accumulate the list, this removes duplicates

Mario Carneiro (Jan 02 2019 at 17:23):

and the only thing you ever put in the list is (twice)

Mario Carneiro (Jan 02 2019 at 17:24):

use :: instead

Koundinya Vajjha (Jan 02 2019 at 17:25):

Aha! that worked. Thanks @Mario Carneiro

Kenny Lau (Jan 02 2019 at 17:33):

anticlimax...

Johan Commelin (Jan 02 2019 at 18:25):

@Koundinya Vajjha Have you seen https://github.com/leanprover/mathlib/blob/master/docs/extras/tactic_writing.md? I have no idea about your level of experience with Lean or other programming languages. But for mathematicians who have never written anything in a functional programming language before, I think this is a very good introduction.


Last updated: Dec 20 2023 at 11:08 UTC