redo_determinism...?

[Andrew Kent]

In Smallstep.v, I'm looking at "redo_determinism" and I'm not seeing what the exercise actually is. It seems to me like they allude to the idea of you "re-verifying determinism," but then they proceed to give you an informal proof. Oddly then the next exercise ("step_deterministic") is an exercise whose goal is to formally proves the deterministic property of the new "step" definition (which is what I thought "redo_determinism" *would* have been).

What am I missing here?

-Andrew

[Jay McCarthy]

I think it is a typo in the textbook generator script and the proof
sketch wasn't meant to be included in the output :)

> --
> You received this message because you are subscribed to the Google Groups
> "byu-cs-430-winter-2013" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to byu-cs-430-winter...@googlegroups.com.
> For more options, visit https://groups.google.com/groups/opt_out.
>
>



--
Jay McCarthy <j...@cs.byu.edu>
Assistant Professor / Brigham Young University
http://faculty.cs.byu.edu/~jay

"The glory of God is Intelligence" - D&C 93