todo.txt

- Something wrong with AllArguments. Test case:
replicate :: n: Nat -> x: Int -> {List {Int | _v == x} | len _v == n}
replicate = \n. \x. if n <= 0 then Nil else Cons x (replicate (dec n) x)


- Type classes (for type variables and abstract datatypes)
- Symmetry reduction

- Examples to make work:
  - More complex uses of indexed list (e.g. reverse, Okazaki)
  - Jeevana's/Leon's desugaring
  - foldl
  - AVL trees without auxiliary functions  

- Mutual recursion
- Irrefutable type errors (like symbol not in scope)
- Check that the first constructor is the base case
- Multisets
- Named arguments for abstract predicates
- Intersection types (carry multiple environments and type constraint checkers), good example: allPos :: (List Int -> Bool) &&& (List Pos -> {Bool | _v}) &&& ({List Nonpos | len _v > 0} -> {Bool | !_v})