search

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring
11 stars 6 forks source link

Should I prove WHILE_true_nonterm in Assignment08_09? #108

Closed ik1ne closed 9 years ago

ik1ne commented 9 years ago 
Require Export Assignment08_08.

(* problem #09: 10 points *)

(** **** Exercise: 2 stars (WHILE_true)  *)
(** Prove the following theorem. _Hint_: You'll want to use
    [WHILE_true_nonterm] here. *)
...

Should I copy&paste it from Equiv.v? SearchAbout WHILE_true_nonterm yields nothing in Assignment08_09.v .

gilhur commented 9 years ago

It is ok to copy&paste it from Equiv.v.