Changes between Version 1 and Version 2 of TypeNats/Axioms


Ignore:
Timestamp:
Nov 27, 2010 9:03:19 PM (4 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Axioms

    v1 v2  
    1 These are just incomplete notes! 
     1(NOTE: This is work in progress) 
     2 
     3These axioms are used by GHC's solver to construct proofs/evidence for various predicates involving type-level naturals. 
     4 
     5The actual algorithm for constructing the evidence is described as set of rules (interactions) which are described separately. 
     6 
    27 
    38 
     
    1116Comparison: 
    1217{{{ 
    13 leqDef:   m <= n    -- if "m <= n" 
    14 leqLeast: 0 <= t 
    15 leqRefl:  t <= t 
    16 leqTrans: (r <= s, s <= t) => r <= t 
     18leqDef:      m <= n    -- if "m <= n" 
     19leqLeast:    0 <= t 
     20leqRefl:     t <= t 
     21leqTrans:    (r <= s, s <= t) => r <= t 
    1722}}} 
    1823