[isabelle] the definition of minus
I noticed the definition to minus today (Isabelle2008):
diff_0: "m - 0 = (m::nat)"
| diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
I was expecting it to be:
diff_0: "0 - m = 0"
| diff_Suc: "(Suc m) - n = (case n of 0 => (Suc m) | Suc k => m - k)"
which I think would produce better code and seems more "natural" to
me... so I thought I was probably missing some subtlety... I'd be
interested in any reasons for the Isabelle definition.
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
This archive was generated by a fusion of
Pipermail (Mailman edition) and