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

Merge pull request #101 from luochen1990/feat-reimpl-rig

Browse Source 
reimpl: rigPlus & rigMult in Core/TT
This commit is contained in:
Edwin Brady 2019-09-20 17:36:53 +01:00 committed by GitHub
commit 8a255da8ea
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
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 Rig1 = "Rig1"
show RigW = "RigW" 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 export
rigPlus : RigCount -> RigCount -> RigCount rigPlus : RigCount -> RigCount -> RigCount
rigPlus Rig0 Rig0 = Rig0 rigPlus a b = fromInt (toInt a + toInt b)
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
export export
rigMult : RigCount -> RigCount -> RigCount rigMult : RigCount -> RigCount -> RigCount
rigMult Rig0 Rig0 = Rig0 rigMult a b = fromInt (toInt a * toInt b)
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
public export public export
data Binder : Type -> Type where data Binder : Type -> Type where