Changes between Version 1 and Version 2 of TypeNats/Axioms
 Timestamp:
 Nov 27, 2010 9:03:19 PM (4 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeNats/Axioms
v1 v2 1 These are just incomplete notes! 1 (NOTE: This is work in progress) 2 3 These axioms are used by GHC's solver to construct proofs/evidence for various predicates involving typelevel naturals. 4 5 The actual algorithm for constructing the evidence is described as set of rules (interactions) which are described separately. 6 2 7 3 8 … … 11 16 Comparison: 12 17 {{{ 13 leqDef: m <= n  if "m <= n"14 leqLeast: 0 <= t15 leqRefl: t <= t16 leqTrans: (r <= s, s <= t) => r <= t18 leqDef: m <= n  if "m <= n" 19 leqLeast: 0 <= t 20 leqRefl: t <= t 21 leqTrans: (r <= s, s <= t) => r <= t 17 22 }}} 18 23