git.iko.soy/Idris-dev
on master help sign in
Fix to get the nat.idr file working correctly. Some sort of bug or misunderstanding in how infix operators are being exported from the algebra.idr file.
066b356Dominic Mulligan
lib/prelude/algebra.idr+6−1
compare with master
unifiedsplit
@@ -4,6 +4,11 @@ import builtins
4
4
5%access public
5%access public
6
6
7+-- XXX: change?
8+infix 6 <->
9+infix 6 <+>
10+infix 6 <*>
11+
7-- Sets equipped with a single binary operation that is associative. Must
12-- Sets equipped with a single binary operation that is associative. Must
8-- satisfy the following laws:
13-- satisfy the following laws:
9-- Associativity of <+>:
14-- Associativity of <+>:
@@ -36,7 +41,7 @@ class Semigroup a => Monoid a where
36class Monoid a => Group a where
41class Monoid a => Group a where
37 inverse : a -> a
42 inverse : a -> a
38
43
39−(<->) : (Group a) => a -> a -> a
44+(<->) : Group a => a -> a -> a
40(<->) left right = left <+> (inverse right)
45(<->) left right = left <+> (inverse right)
41
46
42-- Sets equipped with a single binary operation that is associative and
47-- Sets equipped with a single binary operation that is associative and
lib/prelude/nat.idr+29−31
@@ -85,37 +85,35 @@ record Multiplicative : Set where
85record Additive : Set where
85record Additive : Set where
86 getAdditive : Nat -> Additive
86 getAdditive : Nat -> Additive
87
87
88+-- XXX: infix operators don't seem to be being exported correctly from
89+-- algebra.idr?
88−instance Semigroup Multiplicative where
90+--instance Monoid Multiplicative where
91+-- neutral = getMultiplicative $ S O
89− left <.> right = getMultiplicative $ left' * right'
92+-- left <+> right = getMultiplicative $ left' * right'
90− where
93+-- where
91− left' : Nat
94+-- left' : Nat
92− left' =
95+-- left' =
93− case left of
96+-- case left of
94− getMultiplicative m => m
97+-- getMultiplicative m => m
95−
98+
96− right' : Nat
99+-- right' : Nat
97− right' =
100+-- right' =
98− case right of
101+-- case right of
99− getMultiplicative m => m
102+-- getMultiplicative m => m
100−
103+
101−instance Semigroup Additive where
104+--instance Monoid Additive where
105+-- neutral = getAdditive $ O
102− left <.> right = getAdditive $ left' + right'
106+-- left <+> right = getAdditive $ left' + right'
103− where
107+-- where
104− left' : Nat
108+-- left' : Nat
105− left' =
109+-- left' =
106− case left of
110+-- case left of
107− getAdditive m => m
111+-- getAdditive m => m
108−
112+
109− right' : Nat
113+-- right' : Nat
110− right' =
114+-- right' =
111− case right of
115+-- case right of
112− getAdditive m => m
116+-- getAdditive m => m
113−
114−instance Monoid Multiplicative where
115− neutral = getMultiplicative $ S O
116−
117−instance Monoid Additive where
118− neutral = getAdditive $ O
119
117
120--------------------------------------------------------------------------------
118--------------------------------------------------------------------------------
121-- Auxilliary notions
119-- Auxilliary notions