giltho
commented
2 months ago - clean out unnecessary functions
- remove more unnecessary functions
- somehow even more unnecessary functions?
- add exists to Gillian exprs
- binders of exists are not ins of the expression
- Do the same thing for lstlen in vars
- subst_expr_in_expr will not substitute binders
- perform the correct subst?
- slightly more efficient?
- kill dead code computing constraints for typing
- lemmas without proofs need not have a matching plan for the post condition
- specs can be trusted