diff -r f662831459de -r b550d2c6ca90 doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs Wed Feb 14 10:06:13 2007 +0100 @@ -0,0 +1,51 @@ +module Classes where { + +import Nat; +import Integer; + +class Semigroup a where { + mult :: a -> a -> a; +}; + +class (Semigroup a) => Monoidl a where { + neutral :: a; +}; + +class (Monoidl a) => Group a where { + inverse :: a -> a; +}; + +inverse_int :: Integer -> Integer; +inverse_int i = negate i; + +neutral_int :: Integer; +neutral_int = 0; + +mult_int :: Integer -> Integer -> Integer; +mult_int i j = i + j; + +instance Semigroup Integer where { + mult = mult_int; +}; + +instance Monoidl Integer where { + neutral = neutral_int; +}; + +instance Group Integer where { + inverse = inverse_int; +}; + +pow_nat :: (Monoidl a) => Nat -> a -> a; +pow_nat (Suc n) x = mult x (pow_nat n x); +pow_nat Zero_nat x = neutral; + +pow_int :: (Group a) => Integer -> a -> a; +pow_int k x = + (if 0 <= k then pow_nat (nat k) x + else inverse (pow_nat (nat (negate k)) x)); + +example :: Integer; +example = pow_int 10 (-2); + +}