search

jjdishere / EG

Formalizing Euclidean Geometry in Lean
26 stars 57 forks source link

`Type _` -> `Type*` #297

Closed FR-vdash-bot closed 5 months ago

mbkybky commented 5 months ago

Do we need to change 'Type u' into 'Type*'?

jjdishere commented 5 months ago

Do we need to change 'Type u' into 'Type*'?

I support this idea.