search

math-comp / mcb

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

The simplify_me lemma in sect 2.4 won't compile #6

Closed anton-trunov closed 7 years ago

anton-trunov commented 7 years ago

Lemma simplify_me : size [::] = 0. won't compile because we can't infer the type of the elements of the empty sequence.

amahboubi commented 7 years ago

Thanks for spotting this! Commit 433982ae6419d97d589c3d1f3be1b97edf3b9bff should solve this issue...