Changeset 1515 for src/utilities/binary
 Timestamp:
 Nov 18, 2011, 1:03:14 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/binary/positive.ma
r1330 r1515 656 656 definition minus ≝ λn,m. match partial_minus n m with [ MinusPos p ⇒ p  _ ⇒ one ]. 657 657 658 interpretation " naturalminus" 'minus x y = (minus x y).658 interpretation "positive minus" 'minus x y = (minus x y). 659 659 660 660 lemma partialminus_S: ∀n,m:Pos. … … 942 942 ]. 943 943 944 theorem eqb_elim : ∀ n,m:Pos.∀ P:bool → Prop.944 theorem eqb_elim : ∀ n,m:Pos.∀ P:bool → Type[0]. 945 945 (n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)). 946 946 #n elim n; … … 1159 1159 1160 1160 definition two_power_pos : Pos → Pos ≝ λp.two_power_nat (nat_of_pos p). 1161 1162 1163 1164 definition max : Pos → Pos → Pos ≝ 1165 λn,m. match leb n m with [ true ⇒ m  _ ⇒ n].
Note: See TracChangeset
for help on using the changeset viewer.