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?
Did you find the reason?
Last updated: Jun 01 2023 at 11:01 UTC