Commit History

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