Commit History

Author SHA1 Message Date
  hydraz 954c02672b Add some context to type errors 1 year ago
  hydraz ef437e8177 That's redundant. 1 year ago
  hydraz fcf5a0be54 Instantiation of Pi binders incurs a Set-ness constraint 1 year ago
  hydraz 5a437b8dc1 Normalise top-level terms to their fixed point 1 year ago
  hydraz ccced2c25d Make example even more complex 1 year ago
  hydraz a9a9195be8 Insert type and value in lets 1 year ago
  hydraz 873a59abe5 Print reasons in more cases 1 year ago
  hydraz 385d631424 ... ditto 1 year ago
  hydraz 6ed8b11d80 Format better 1 year ago
  hydraz dc7c1be712 Add sugar for repeated binding groups 1 year ago
  hydraz a805a6764b Add the binder sugar to Pi types 1 year ago
  hydraz 9dccdf575f Add some destructuring to the example 1 year ago
  hydraz f7a736ec75 Remove trace 1 year ago
  hydraz d7fe8d414a Make constructors a tiny bit less stupid 1 year ago
  hydraz 059df204cf Generate `Equal` instead of `Instance` for defined variables 1 year ago
  hydraz 424bdfd0fd Move to a constraint-based unification engine 1 year ago
  hydraz 572f33719c Fix *all* hlint hints 1 year ago
  hydraz 1a5724c8aa Make example Eq silliness again 1 year ago
  hydraz d0aea0f31c Improve printing of errors 1 year ago
  hydraz deba09e09e Irrelevant variables don't matter for consistency checking. 1 year ago
  hydraz 8ce513c834 Allow multiple bindings in a single lambda 1 year ago
  hydraz 90415584d7 Improve type error quality 1 year ago
  hydraz eb08c80fe2 Remove Eq inductive type from example 1 year ago
  hydraz 3b1aa16cf1 Use /\ 1 year ago
  hydraz 7c717c476e Infer `let`s correctly. 1 year ago
  hydraz f8d662ae4c Remove traces of impurity 1 year ago
  hydraz d16db1cb5d Print definitions if they exist 1 year ago
  hydraz 02b8233532 Introduce /\ syntax for type parameters 1 year ago
  hydraz d2fbe3f913 Improve pretty printing of Pi abstractions 1 year ago
  hydraz 85a386b3dc Add sugar for Set 0 1 year ago