Stream: math-comp devs

Topic: subtype

Laurent Théry (Jun 01 2022 at 12:18):

while porting some files from a tutorial by assia (here)
It seems that before we could write

Definition two'' : 'I_3 := Sub 2 (refl_equal true).

but now we have to write.

Definition two'' : [subType of 'I_3] := Sub 2 (refl_equal true).

What has changed?

Last updated: Aug 11 2022 at 01:03 UTC