Changes between Version 22 and Version 23 of IntermediateTypes


Ignore:
Timestamp:
Aug 4, 2006 4:08:08 PM (8 years ago)
Author:
guest
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • IntermediateTypes

    v22 v23  
    173173would result in a data constructor with type 
    174174{{{ 
    175   T1 :: forall a b. forall a1 b1. (a :=: [a1], b :=: (a1, b1)) => a1 -> b1 -> T a b 
     175T1 :: forall a b. forall a1 b1. (a :=: [a1], b :=: (a1, b1)) => a1 -> b1 -> T a b 
    176176}}} 
    177177This means that (unlike in the previous intermediate language) all data constructor return types have the form `T a1 ... an` where 
     
    223223In the paper we'd write 
    224224{{{ 
    225         axiom CoT : (forall t. T t) :=: (forall t. [t]) 
     225axiom CoT : (forall t. T t) :=: (forall t. [t]) 
    226226}}} 
    227227and then when we used `CoT` at a particular type, `s`, we'd say 
    228228{{{ 
    229         CoT @ s 
     229CoT @ s 
    230230}}} 
    231231which encodes as `(TyConApp instCoercionTyCon [TyConApp CoT [], s])`