Christophe Raffalli
Christophe Raffalli
Mutually inductive types can be encoded using extra parameters, but this result in a notion of sized type which is not the one we want, and leads to failure of...
various forbidden case due to sorting that have no error generated
Printing has been improved, but is not finished ... quite a few syntactic sugar are missing. Notably terms in values, cons, nil, infix, ...
When writing let f = fun x ... or even applications, or dependant product, we have no short way to indicate the current totality we want. Do we need something...
Here, we put all use case that seems to be solvable (or that even work in subml): This issue should probably never be closed. - test/fifo.pml: with a pair of...
Some time, extra information comes from typing which allows to restrict cases. This information is probably available in the type of the VWit ... We should try to use it!...
Currently, we use in subtyping a heuristic testing is the term (int t : A < B) is a value. This heuristic seems in fact to test if we already...
When we learn that functions are equal, we should keep that information: VN_LAbs should contain a list of functions. This would allow to always deduce f x = g x...
insert_t_node should use a stack to avoid creating node for partially applied function. For instance, adding [add n p] to the pool also adds [add n] which is a lambda,...
In function which are very frequently called, log and chrono can cost a lot. If I uncomment the log in add_term and add_valu, the cost of log+chorno in Equiv and...