search

gmalecha / mirror-core

A framework for extensible, reflective decision procedures.
Other
19 stars 5 forks source link

Prove Expr_expr is ExprOk #13

Closed gmalecha closed 10 years ago

gmalecha commented 10 years ago

ExprOk needs a weakening proof but that requires ExprD. This will require a little bit of refactoring.

I think the solution is to put Expr_expr in Expr.v

gmalecha commented 10 years ago

Done with reorg/proving (5be9410954df7a1abb5deb931718ee36c95b98a6)