search

PrincetonUniversity / VST

Verified Software Toolchain
https://vst.cs.princeton.edu
Other
425 stars 91 forks source link

More concise defined evaluations (Definition arch : nat := Eval ... ) #690

Open andrew-appel opened 1 year ago

andrew-appel commented 1 year ago

An anonymous referee of a CoqPL submission suggests,

https://github.com/PrincetonUniversity/VST/blob/6bcedd6e987cea40fe577540782f88d85be687dd/lib/proof/spec_math.v#L31

Why not

Definition arch : nat := Eval vm_compute in arch'.

same for GNU_errors just below