search

math-comp / mcb

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

Sect. 3.1.2: "isT : true is a valid proof of (0 < n.+1)" is a bit misleading #55

Closed anton-trunov closed 6 years ago

anton-trunov commented 6 years ago

The term (isT : true) is a valid proof of (0 < n.+1), as well as a proof of (0 != p.+1).

The section should probably remind the reader that isT has type is_true true because of the coercion mechanism.