idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-15 22:32:19 +03:00
Code Issues Projects Releases Wiki Activity

Simplify 01W Preorder

Browse Source
This commit is contained in:
Nick Drozd 2021-07-07 23:54:54 -05:00 committed by G. Allais
parent 5d70c746b1
commit b918f1c105
1 changed files with 15 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
src/Algebra/ZeroOneOmega.idr
View File

@ -10,23 +10,22 @@ data ZeroOneOmega = Rig0 | Rig1 | RigW
export
Preorder ZeroOneOmega where
Rig0 <= _ = True
Rig0 <= _ = True
Rig1 <= Rig1 = True
Rig1 <= RigW = True
RigW <= RigW = True
_ <= _ = False
_ <= RigW = True
_ <= _ = False
preorderRefl {x = Rig0} = Refl
preorderRefl {x = Rig1} = Refl
preorderRefl {x = RigW} = Refl
preorderTrans {x = Rig0} {y = y} {z = z} a b = Refl
preorderTrans {x = Rig1} {y = Rig0} {z = Rig0} Refl Refl impossible
preorderTrans {x = Rig1} {y = Rig1} {z = Rig0} _ Refl impossible
preorderTrans {x = Rig1} {y = RigW} {z = Rig0} _ Refl impossible
preorderTrans {x = Rig1} {y = y} {z = Rig1} a b = Refl
preorderTrans {x = Rig1} {y = y} {z = RigW} a b = Refl
preorderTrans {x = RigW} {y = Rig0} {z = _} Refl _ impossible
preorderTrans {x = RigW} {y = Rig1} {z = _} Refl _ impossible
preorderTrans {x = RigW} {y = RigW} {z = z} a b = b
preorderTrans {x = Rig0} _ _ = Refl
preorderTrans {x = Rig1} {y = Rig0} _ _ impossible
preorderTrans {x = Rig1} {y = Rig1} _ yz = yz
preorderTrans {x = Rig1} {y = RigW} {z = Rig0} _ _ impossible
preorderTrans {x = Rig1} {y = RigW} {z = Rig1} _ _ = Refl
preorderTrans {x = Rig1} {y = RigW} {z = RigW} _ _ = Refl
preorderTrans {x = RigW} {y = Rig0} _ _ impossible
preorderTrans {x = RigW} {y = Rig1} _ _ impossible
preorderTrans {x = RigW} {y = RigW} _ yz = yz
public export
Eq ZeroOneOmega where
@ -45,9 +44,7 @@ export
rigPlus : ZeroOneOmega -> ZeroOneOmega -> ZeroOneOmega
rigPlus Rig0 a = a
rigPlus a Rig0 = a
rigPlus Rig1 a = RigW
rigPlus a Rig1 = RigW
rigPlus RigW RigW = RigW
rigPlus _ _ = RigW
export
rigMult : ZeroOneOmega -> ZeroOneOmega -> ZeroOneOmega
@ -55,7 +52,8 @@ rigMult Rig0 _ = Rig0
rigMult _ Rig0 = Rig0
rigMult Rig1 a = a
rigMult a Rig1 = a
rigMult RigW RigW = RigW
rigMult _ _ = RigW
public export
Semiring ZeroOneOmega where