# Zulip Chat Archive

## Stream: general

### Topic: statement linter

#### Patrick Massot (Jul 25 2018 at 22:20):

I have a new challenge in the same style as the `print_names`

command, but harder. We all know how to produce the list of everything defined in the current Lean file. Now we want to filter the result, keeping only lemmas or theorems whose input contains two instances for the same type class. For instance, running this command in https://github.com/leanprover/mathlib/blob/master/analysis/topology/continuity.lean must return (among others) `is_closed_diagonal`

since:

import analysis.topology.continuity #check @is_closed_diagonal /- is_closed_diagonal : ∀ {α : Type u_1} [_inst_1 : topological_space α] [_inst_4 : topological_space α] [_inst_5 : t2_space α], is_closed {p : α × α | p.fst = p.snd} -/

(this is due to instance explicitly asked for in the statement but already present as variables).

#### Reid Barton (Jul 25 2018 at 23:19):

oops!

#### Simon Hudon (Jul 26 2018 at 00:34):

Hint: if `t`

is the type of `is_closed_diagonal`

, `t.is_pi`

will return `tt`

(true) because `t`

is a pi type (the assumptions are basically function arguments). `t.binding_domain`

will gives you the type of the first assumption or variable (i.e. `Type u_1`

) and `t.binding_body`

will be the rest (i.e. `∀ [_inst_1 : topological_space α] [_inst_4 : topological_space α] [_inst_5 : t2_space α], is_closed {p : α × α | p.fst = p.snd}`

). Look at their definition and write a `arguments : expr → tactic (list expr)`

function. This will bring you closer to a solution.

#### Patrick Massot (Jul 26 2018 at 07:58):

Thank you very much, I'll try to work on this exercise soon (but not right now).

Last updated: May 12 2021 at 05:19 UTC