Tactic help

Stream: general

[Koundinya Vajjha]

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]

you used insert to accumulate the list, this removes duplicates

[Mario Carneiro]

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

[Mario Carneiro]

use :: instead

[Koundinya Vajjha]

Aha! that worked. Thanks @Mario Carneiro

[Kenny Lau]

anticlimax...

[Johan Commelin]

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