From b078ef9a2268e8d9b5de92269952a37e348e8947 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Wed, 22 Jul 2020 14:30:47 -0700
Subject: [PATCH] Remove implicit arguments from TypsafeIntrV2.

---
 code/typesafe-interpreter/TypesafeIntrV2.idr | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/code/typesafe-interpreter/TypesafeIntrV2.idr b/code/typesafe-interpreter/TypesafeIntrV2.idr
index 5888445..ea01d17 100644
--- a/code/typesafe-interpreter/TypesafeIntrV2.idr
+++ b/code/typesafe-interpreter/TypesafeIntrV2.idr
@@ -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