Closed nilehmann closed 6 months ago
Make assoc pred applications/alias pred part of the syntax of Expr in rty. Encoding into fixpoint assumes that assoc preds can only be used at the top level in the surface syntax, but the restriction could easily be lifted.
Expr
rty
Make assoc pred applications/alias pred part of the syntax of
Exprinrty. Encoding into fixpoint assumes that assoc preds can only be used at the top level in the surface syntax, but the restriction could easily be lifted.