redtt icon indicating copy to clipboard operation
redtt copied to clipboard
verified publisher icon RedPRL

Remove mortality in the coe of extension types

Open favonia opened this issue 7 years ago • 1 comments

The following line is always a no-op.

https://github.com/RedPRL/redtt/blob/9392635a6c7dcb7b3afddab8ef5210308426ea36/src/core/Val.ml#L1716

This is fixed in #270, but I want to document this.

favonia avatar Sep 29 '18 14:09 favonia

I should let GitHub close it.

favonia avatar Sep 30 '18 00:09 favonia