projects
/
coq-hetmet.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
GArrowSkeleton: add comment
[coq-hetmet.git]
/
examples
/
GArrowSkeleton.hs
diff --git
a/examples/GArrowSkeleton.hs
b/examples/GArrowSkeleton.hs
index
dd7937b
..
9f42e8a
100644
(file)
--- a/
examples/GArrowSkeleton.hs
+++ b/
examples/GArrowSkeleton.hs
@@
-18,9
+18,11
@@
-- behavior below -- you'd get (GAS_comp f GAS_id) instead of f. In
-- practice this means that the user must be prepared for the skeleton
-- TikZ diagram to be a nondeterministically-chosen boxes-and-wires
-- behavior below -- you'd get (GAS_comp f GAS_id) instead of f. In
-- practice this means that the user must be prepared for the skeleton
-- TikZ diagram to be a nondeterministically-chosen boxes-and-wires
--- diagram which ks *equivalent to* the term, rather than structurally
+-- diagram which is *equivalent to* the term, rather than structurally
-- exactly equal to it.
--
-- exactly equal to it.
--
+-- A normal form theorem and normalization algorithm are being prepared.
+--
module GArrowSkeleton (GArrowSkeleton(..), optimize, beautify)
where
import Prelude hiding ( id, (.), lookup, repeat )
module GArrowSkeleton (GArrowSkeleton(..), optimize, beautify)
where
import Prelude hiding ( id, (.), lookup, repeat )