Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Remove implicit arguments from TypsafeIntrV2.

Browse Source
This commit is contained in:
Danila Fedorin 2020-07-22 14:30:47 -07:00
parent fdaec6d5a9
commit b078ef9a22
1 changed files with 9 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
code/typesafe-interpreter/TypesafeIntrV2.idr
View File

@ -18,15 +18,15 @@ boolStringImpossible : BoolType = StringType -> Void
boolStringImpossible Refl impossible
decEq : (a : ExprType) -> (b : ExprType) -> Dec (a = b)
decEq {a = IntType} {b = IntType} = Yes Refl
decEq {a = BoolType} {b = BoolType} = Yes Refl
decEq {a = StringType} {b = StringType} = Yes Refl
decEq {a = IntType} {b = BoolType} = No intBoolImpossible
decEq {a = BoolType} {b = IntType} = No $ intBoolImpossible . sym
decEq {a = IntType} {b = StringType} = No intStringImpossible
decEq {a = StringType} {b = IntType} = No $ intStringImpossible . sym
decEq {a = BoolType} {b = StringType} = No boolStringImpossible
decEq {a = StringType} {b = BoolType} = No $ boolStringImpossible . sym
decEq IntType IntType = Yes Refl
decEq BoolType BoolType = Yes Refl
decEq StringType StringType = Yes Refl
decEq IntType BoolType = No intBoolImpossible
decEq BoolType IntType = No $ intBoolImpossible . sym
decEq IntType StringType = No intStringImpossible
decEq StringType IntType = No $ intStringImpossible . sym
decEq BoolType StringType = No boolStringImpossible
decEq StringType BoolType = No $ boolStringImpossible . sym
data Op
= Add