Open gebner opened 2 years ago
Synport:
namespace Bool theorem coe_sort_tt : coeSort.{1, 1} true = True := coe_sort_tt
In Lean 3 coe_sort_tt would resolve to _root_.coe_sort_tt resulting in a non-recursive alias definition. But in Lean 4, coe_sort_tt now resolves to Bool.coe_sort_tt and we get a (nonterminating) recursive definition.
coe_sort_tt
_root_.coe_sort_tt
Bool.coe_sort_tt
Synport:
In Lean 3
coe_sort_ttwould resolve to_root_.coe_sort_ttresulting in a non-recursive alias definition. But in Lean 4,coe_sort_ttnow resolves toBool.coe_sort_ttand we get a (nonterminating) recursive definition.