Changes between Version 1 and Version 2 of TypeNats/Axioms


Ignore:
Timestamp:
Nov 27, 2010 9:03:19 PM (5 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