Module Dcalc.Invariants

Check all invariants. Return true if all the invariants are correct. Print errors messages for each unsucessfull invariants. Here are all the invariants checked:

• invariant_default_no_arrow check no default term has a function type.
• invariant_no_partial_evaluation check there is no partial function.
• invariant_no_return_a_function check no function return a function.
• invariant_app_inversion : if the term is an function application, then there is only 5 possibility : it is a let binding, it is an operator application, it is an variable application, it is a struct access function application (sub-scope call), or it is a operator application with trace.
• invariant_match_inversion : if a term is a match, then every branch is an function abstraction.