-
Type class constraints in functions
-
Polymorphic application of functions (i.e. find natural transformations)
-
Relations
-
Imperative programs
-
Hide output of background theories
- Can we safely disable (or limit) completion with background theories?
- Explore background theories up to a smaller size
- Remember the set of terms and add to it
-
Add QS1 feature of organising laws by defining function (i.e., "this is a law about BLAH")
-
Improve handling of partial functions (see Heaps.hs)
-
Make Type into an abstract type