Skip to content

Make exprIsConApp_maybe use MCoercion

In exprIsConApp_maybe we have

data ConCont = CC [CoreExpr] Coercion

But the Coercion is almost always Refl. We have MCoercion for this exact purpose.

Idea: just replace Coercion by MCoercion. Simpler, more direct, and perhaps a tiny bit more efficient.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information