Changes between Version 14 and Version 15 of InjectiveTypeFamilies


Ignore:
Timestamp:
Oct 10, 2014 2:08:30 PM (5 years ago)
Author:
jstolarek
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • InjectiveTypeFamilies

    v14 v15  
    231231
    2322322. When checking equation of an open type family we try to unify its RHS with
    233    RHSs of all equations we've seen so far. If we succeed this means that this type
    234    family is not injective because two non-overlapping equations can produce types
    235    that can be unified.
     233   RHSs of all equations we've seen so far. If we succeed then LHSs of unified
     234   equations must be identical under that substitution. If they are not identical
     235   then we declare that a type family is not injective.
    236236
    237237Closed type families