math-comp / mcb

Mathematical Components (the Book)
Other
140 stars 25 forks source link

More details needed in fiddling with packed classes #101

Open amahboubi opened 4 years ago

amahboubi commented 4 years ago

End of section 8.4 , in the definition of pack : provide a type annotation for m and explain why m0 cannot be used as such, as in Pack (@Class T b m0).