edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-24 12:54:28 +03:00
Code Issues Projects Releases Wiki Activity

reimpl: rigPlus & rigMult in Core/TT

Browse Source
This commit is contained in:
LuoChen 2019-09-20 12:43:25 +08:00
parent 2f20f7e136
commit 8d5f72c762
1 changed files with 12 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
src/Core/TT.idr
View File

@ -231,29 +231,23 @@ Show RigCount where
show Rig1 = "Rig1"
show RigW = "RigW"
fromInt : Int -> RigCount
fromInt 0 = Rig0
fromInt 1 = Rig1
fromInt _ = RigW
toInt : RigCount -> Int
toInt Rig0 = 0
toInt Rig1 = 1
toInt RigW = 2
export
rigPlus : RigCount -> RigCount -> RigCount
rigPlus Rig0 Rig0 = Rig0
rigPlus Rig0 Rig1 = Rig1
rigPlus Rig0 RigW = RigW
rigPlus Rig1 Rig0 = Rig1
rigPlus Rig1 Rig1 = RigW
rigPlus Rig1 RigW = RigW
rigPlus RigW Rig0 = RigW
rigPlus RigW Rig1 = RigW
rigPlus RigW RigW = RigW
rigPlus a b = fromInt (toInt a + toInt b)
export
rigMult : RigCount -> RigCount -> RigCount
rigMult Rig0 Rig0 = Rig0
rigMult Rig0 Rig1 = Rig0
rigMult Rig0 RigW = Rig0
rigMult Rig1 Rig0 = Rig0
rigMult Rig1 Rig1 = Rig1
rigMult Rig1 RigW = RigW
rigMult RigW Rig0 = Rig0
rigMult RigW Rig1 = RigW
rigMult RigW RigW = RigW
rigMult a b = fromInt (toInt a * toInt b)
public export
data Binder : Type -> Type where