Changes between Version 22 and Version 23 of IntermediateTypes

Timestamp:

08/04/06 09:08:08 (7 years ago)

Author:

guest

Comment:

--

IntermediateTypes

@@ -173 +173 @@
 would result in a data constructor with type
 {{{
-  T1 :: forall a b. forall a1 b1. (a :=: [a1], b :=: (a1, b1)) => a1 -> b1 -> T a b
+T1 :: forall a b. forall a1 b1. (a :=: [a1], b :=: (a1, b1)) => a1 -> b1 -> T a b
 }}}
 This means that (unlike in the previous intermediate language) all data constructor return types have the form `T a1 ... an` where
@@ -223 +223 @@
 In the paper we'd write
 {{{
-        axiom CoT : (forall t. T t) :=: (forall t. [t])
+axiom CoT : (forall t. T t) :=: (forall t. [t])
 }}}
 and then when we used `CoT` at a particular type, `s`, we'd say
 {{{
-        CoT @ s
+CoT @ s
 }}}
 which encodes as `(TyConApp instCoercionTyCon [TyConApp CoT [], s])`