search

math-comp / mcb

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

Typo page 56: incorrect Definition #87

Open usr345 opened 4 years ago

usr345 commented 4 years ago

On page 56 the Definition says: Definition leq n m := m - n == 0.

It should be: Definition leq m n := m - n == 0.

It references to page 26 of Chapter 1, which has the correct definition:

Definition leq m n := m - n == 0.

gares commented 4 years ago

Thanks

usr345 commented 4 years ago

@gares On page 119 no need to put "@" before Pack:

Definition nat_eqType : eqType := @Pack nat eqn. And before eq_op:

Check (@eq_op nat_eqType 3 4).