idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-24 06:52:19 +03:00
Code Issues Projects Releases Wiki Activity

Remove more trailing whitespace

Browse Source
This commit is contained in:
Edwin Brady 2021-03-03 14:36:33 +00:00
parent 6a29fab245
commit c9de4d9f9f
1 changed files with 23 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

46
tests/idris2/interface024/EH.idr
View File

@ -12,20 +12,20 @@ interface Additive a where
interface Additive2 a where
constructor MkAdditive2
(:+:) : a -> a -> a
O2 : a
O2 : a
interface Multiplicative a where
constructor MkMultiplicative
(.*.) : a -> a -> a
I : a
record MonoidOver U where
record MonoidOver U where
constructor WithStruct
Unit : U
Mult : U -> U -> U
lftUnit : (x : U) -> Unit `Mult` x = x
rgtUnit : (x : U) -> x `Mult` Unit = x
assoc : (x,y,z : U)
assoc : (x,y,z : U)
-> x `Mult` (y `Mult` z) = (x `Mult` y) `Mult` z
record Monoid where
@ -34,12 +34,12 @@ record Monoid where
Struct : MonoidOver U
AdditiveStruct : (m : MonoidOver a) -> Additive a
AdditiveStruct m = MkAdditive (Mult $ m)
AdditiveStruct m = MkAdditive (Mult $ m)
(Unit $ m)
AdditiveStruct2 : (m : MonoidOver a) -> Additive2 a
AdditiveStruct2 m = MkAdditive2 (Mult $ m)
AdditiveStruct2 m = MkAdditive2 (Mult $ m)
(Unit $ m)
AdditiveStructs : (ma : MonoidOver a) -> (mb : MonoidOver b)
AdditiveStructs : (ma : MonoidOver a) -> (mb : MonoidOver b)
-> (Additive a, Additive2 b)
AdditiveStructs ma mb = (AdditiveStruct ma, AdditiveStruct2 mb)
@ -49,46 +49,46 @@ getAdditive m = AdditiveStruct (Struct m)
MultiplicativeStruct : (m : Monoid) -> Multiplicative (U m)
MultiplicativeStruct m = MkMultiplicative (Mult $ Struct m)
(Unit $ Struct m)
-----------------------------------------------------
-----------------------------------------------------
Commutative : MonoidOver a -> Type
Commutative m = (x,y : a) -> let _ = AdditiveStruct m in
x .+. y = y .+. x
Commute : (Additive a, Additive2 a) => Type
Commute =
(x11,x12,x21,x22 : a) ->
(x11,x12,x21,x22 : a) ->
((x11 :+: x12) .+. (x21 :+: x22))
=
((x11 .+. x21) :+: (x12 .+. x22))
product : (ma, mb : Monoid) -> Monoid
product ma mb =
let
product : (ma, mb : Monoid) -> Monoid
product ma mb =
let
%hint aStruct : Additive (U ma)
aStruct = getAdditive ma
%hint bStruct : Additive (U mb)
bStruct = getAdditive mb
in MkMonoid (U ma, U mb) $ WithStruct
(O, O)
(\(x1,y1), (x2, y2) => (x1 .+. x2, y1 .+. y2))
(\(x,y) => rewrite lftUnit (Struct ma) x in
(\(x,y) => rewrite lftUnit (Struct ma) x in
rewrite lftUnit (Struct mb) y in
Refl)
(\(x,y) => rewrite rgtUnit (Struct ma) x in
rewrite rgtUnit (Struct mb) y in
Refl)
(\(x1,y1),(x2,y2),(x3,y3) =>
(\(x1,y1),(x2,y2),(x3,y3) =>
rewrite assoc (Struct ma) x1 x2 x3 in
rewrite assoc (Struct mb) y1 y2 y3 in
Refl)
EckmannHilton : forall a . (ma,mb : MonoidOver a)
EckmannHilton : forall a . (ma,mb : MonoidOver a)
-> let ops = AdditiveStructs ma mb in
Commute @{ops}
-> (Commutative ma, (x,y : a) -> x .+. y = x :+: y)
EckmannHilton ma mb prf =
EckmannHilton ma mb prf =
let %hint first : Additive a
first = AdditiveStruct ma
%hint second : Additive2 a
@ -97,7 +97,7 @@ EckmannHilton ma mb prf =
SameUnits = Calc $
|~ O
~~ O .+. O ...(sym $ lftUnit ma O)
~~ (O :+: O2) .+. (O2 :+: O) ...(sym $ cong2 (.+.)
~~ (O :+: O2) .+. (O2 :+: O) ...(sym $ cong2 (.+.)
(rgtUnit mb O)
(lftUnit mb O))
~~ (O .+. O2) :+: (O2 .+. O) ...(prf O O2 O2 O)
@ -105,7 +105,7 @@ EckmannHilton ma mb prf =
(lftUnit ma O2)
(rgtUnit ma O2))
~~ O2 ...(lftUnit mb O2)
SameMults : (x,y : a) -> (x .+. y) === (x :+: y)
SameMults x y = Calc $
|~ x .+. y
@ -113,13 +113,13 @@ EckmannHilton ma mb prf =
(rgtUnit mb x)
(lftUnit mb y))
~~ (x .+. O2) :+: (O2 .+. y) ...(prf x O2 O2 y)
~~ (x .+. O ) :+: (O .+. y) ...(cong (\u =>
~~ (x .+. O ) :+: (O .+. y) ...(cong (\u =>
(x .+. u) :+: (u .+. y))
(sym SameUnits))
~~ x :+: y ...(cong2 (:+:)
(rgtUnit ma x)
(lftUnit ma y))
Commutativity : Commutative ma
Commutativity x y = Calc $
|~ x .+. y
@ -127,7 +127,7 @@ EckmannHilton ma mb prf =
(lftUnit mb x)
(rgtUnit mb y))
~~ (O2 .+. y) :+: (x .+. O2) ...(prf O2 x y O2)
~~ (O .+. y) :+: (x .+. O ) ...(cong (\u =>
~~ (O .+. y) :+: (x .+. O ) ...(cong (\u =>
(u .+. y) :+: (x .+. u))
(sym SameUnits))
~~ y :+: x ...(cong2 (:+:)