Coq's Trakt

Stream: lean4

[Tomaz Gomes]

Do we have an equivalent to Coq's tactic "trakt"? I.e. a tactic that is capable of normalizing a goal that mixes Prop and Bool or Nat and Int?

https://ecrancemerce.github.io/trakt/#/demo

[Yaël Dillies]

We have tactic#zify

[Yaël Dillies]

(@Scott Morrison, you might want to update the linkifier!)

[Mario Carneiro]

for prop/bool simp mostly does the job

[Mario Carneiro]

The general description of the trakt tactic looks like transfer though

[Eric Wieser]

Yaël Dillies said:

(Scott Morrison, you might want to update the linkifier!)

There is nothing to link to (yet) for Lean 4

[Yaël Dillies]

I was hoping it would prompt someone to set up the list of tactics again :grinning: