When constructing things inside of the splicer, it's easy to make mistakes and accidentally produce ill-typed terms, which can be really hard to debug. This is especially true when dealing with universes, as it's quite easy to forget an el_in/el_out somewhere and then spend a while reading bad do_el traces to figure out your mistake.
It would be nice to add some sort of optional "splice linter" that could typecheck any terms that it produces against a provided type. This could be used during development, hopefully making life a little less painful!
When constructing things inside of the splicer, it's easy to make mistakes and accidentally produce ill-typed terms, which can be really hard to debug. This is especially true when dealing with universes, as it's quite easy to forget an
el_in/el_outsomewhere and then spend a while readingbad do_eltraces to figure out your mistake.It would be nice to add some sort of optional "splice linter" that could typecheck any terms that it produces against a provided type. This could be used during development, hopefully making life a little less painful!