Hi @leafac! I’m trying to formalize typed arithmetic expressions from types and programming languages book.

My current status is on the following gist: https://gist.github.com/rodrigogribeiro/e0fd3e1e3ff017b614dcfeee9f9154e0

My problem is on improve the test coverage from progress and preservation properties

Currently, all my tries doesn’t trigger any evaluation rules.

I had used the same function for coverage stats from the amb tutorial

and also I had tried to use #:satisfying clause to test progress and preservation only on well typed terms

If anyone could provide me any clue on how could I improve such coverage or what mistake I’m doing, it would be great

Something strikes me as weird in line 118: https://gist.github.com/rodrigogribeiro/e0fd3e1e3ff017b614dcfeee9f9154e0#file-tyexp-rkt-L118 Why the extra parentheses around e? It causes the following strange behavior: > (apply-reduction-relation red (term zero)) '() > (reduces? (term zero)) . . reduction-relation: relation not defined for (zero)

I’d expect that reduces? would fail only iff apply-reduction-relation failed for any given term.

I tried removing the parentheses and got something that looks better:

> (apply-reduction-relation red (term zero))
'()
> (reduces? (term zero))
#f

I don’t think this fully explains your problem. But maybe it’s a start?