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