cv_compute
Folders and files
| Name | Name | Last commit date | ||
|---|---|---|---|---|
parent directory.. | ||||
Examples on using the cv_computeLib library
-------------------------------------------------------------------------------
Name Description
examplesScript.sml Two examples of how to define functions in the :cv
type, for use with cv_computeLib.compute.
cv_golScript.sml An example which uses cv_transLib to evaluate
Conway's Game of Life symbolically.
cv_bootScript.sml An example which applies cv_transLib to the compiler
from HOL/examples/bootstrap.