Changeset 746 for src/ASM/Util.ma
- Timestamp:
- Apr 8, 2011, 11:51:38 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Util.ma
r715 r746 115 115 λm, n: nat. 116 116 leb n m. 117 118 (* dpm: unless I'm being stupid, this isn't defined in the stdlib? *) 119 let rec eq_nat (n: nat) (m: nat) on n: bool ≝ 120 match n with 121 [ O ⇒ match m with [ O ⇒ true | _ ⇒ false ] 122 | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ] 123 ]. 117 124 118 125 (* dpm: conflicts with library definitions
Note: See TracChangeset
for help on using the changeset viewer.