Changeset 2700 for src/ASM/Util.ma
 Timestamp:
 Feb 22, 2013, 2:12:24 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Util.ma
r2673 r2700 784 784 mk_Prod … (m ÷ n) (modulus m n). 785 785 786 let rec exponential (m: nat) (n: nat) on n ≝787 match n with788 [ O ⇒ S O789  S o ⇒ m * exponential m o790 ].791 792 interpretation "Nat exponential" 'exp n m = (exponential n m).793 794 786 notation "hvbox(a break ⊎ b)" 795 787 left associative with precedence 55
Note: See TracChangeset
for help on using the changeset viewer.