Clear true tactic

Stream: Is there code for X?

[Bolton Bailey]

Is there a tactic that will clear all true statements from the local context? This would be useful for me in dealing with a large number of automatically generated equations, many of which simplify to true.

[Kevin Buzzard]

As far as I know we don't, although this strikes me as being an even easier tactic to write for a beginner than the "hello world" tactic, namely assumption.

[Yaël Dillies]

Isn't it exactly what clear does?

[Yaël Dillies]

Or are you saying that you want to simplify hypothesis that aren't true but equal to true? That seems a bit harder.

[Mario Carneiro]

I think the task is to automatically find the list of hypotheses to clear based on the type. clear takes a list of hypotheses, not a type

[Yaël Dillies]

Ah maybe that's the job of the hypothetical clear!

[Alex J. Best]

@Bolton Bailey does using tactic#cases_matching suit your purpose?

import tactic

example (h h' : true) : false :=
begin
  cases_matching* true,
end

[Eric Wieser]

docs#tactic.interactive.cases_matching?

[Alex J. Best]

Thanks! I guess tactic#cases_type is even better actually