Commit 2023-10-14 06:04 8437cdac

View on Github →

chore(Archive,Counterexamples): use Type* not Type _ (#7663) This is an exhaustive replacement.

Estimated changes

modified inductive PropEncodable.PropForm
modified theorem Imo1962Q4.formula
modified theorem Imo1998Q2.add_sq_add_sq_sub
modified theorem AbelRuffini.map_Phi
modified def Theorems100.cut
modified theorem Theorems100.cut_empty_succ
modified theorem Theorems100.cut_insert
modified theorem Theorems100.cut_zero
modified theorem Theorems100.mem_cut
modified theorem Theorems100.partialGF_prop