Stream: math-comp devs

Topic: subtype

view this post on Zulip 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?

view this post on Zulip Anders Larsson (Aug 31 2022 at 06:11):

Did you find the reason?

Last updated: Jun 01 2023 at 11:01 UTC