search

brando90 / cs522_project

0 stars 0 forks source link

proof this #2

Closed brando90 closed 5 years ago

brando90 commented 5 years ago

Exercise: 3 stars (bevalR) Write a relation bevalR in the same style as aevalR, and prove that it is equivalent to beval. Inductive bevalR: bexp → bool → Prop := ( FILL IN HERE ) . Lemma beval_iff_bevalR : ∀ b bv, bevalR b bv ↔ beval b = bv. Proof. ( FILL IN HERE ) Admitted. ☐ End AExp.

https://softwarefoundations.cis.upenn.edu/lf-current/Imp.html

brando90 commented 5 years ago

@umenthum is this done?

umenthum commented 5 years ago

Yes.