bool to Prop

Stream: general

[Yunlong LIN]

↥tt, The up arrow in lean means bool to prop. So how use true to replace ↥tt in lean. And how should we prove when the final goal is ↥tt.

[Scott Morrison]

It's a good habit to try posting a #mwe in your questions. Here for example you could just write:

example : (tt : Prop) :=
begin

end

[Scott Morrison]

There are many ways to solve this. Try

import tactic

example : (tt : Prop) :=
begin
  hint,
end

to see some suggestions.

[Scott Morrison]

That said, this may be an #xy problem... If your final goal is ↥tt my actual suggestion is that you've earlier done something inappropriate.