In ProgramTypeTests.lean, the good_prog test shows DDM translator errors:
Unsupported construct in lopToExpr: 0-ary op not found: fooAliasVal
Unsupported construct in lopToExpr: 0-ary op not found: fooVal
These are function constants defined via type aliases (FooAlias). The DDM translator can't resolve them during the lopToExpr conversion.
In
ProgramTypeTests.lean, thegood_progtest shows DDM translator errors:These are function constants defined via type aliases (
FooAlias). The DDM translator can't resolve them during thelopToExprconversion.