projects
/
coq-hetmet.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
35974aa
)
add commented-out demo
author
Adam Megacz
<megacz@cs.berkeley.edu>
Sat, 14 Apr 2012 21:53:09 +0000
(14:53 -0700)
committer
Adam Megacz
<megacz@cs.berkeley.edu>
Sat, 14 Apr 2012 21:53:09 +0000
(14:53 -0700)
examples/IFLDemos.hs
patch
|
blob
|
history
diff --git
a/examples/IFLDemos.hs
b/examples/IFLDemos.hs
index
43d29f4
..
288e6a4
100644
(file)
--- a/
examples/IFLDemos.hs
+++ b/
examples/IFLDemos.hs
@@
-1,6
+1,14
@@
{-# OPTIONS_GHC -XModalTypes -dcore-lint -XScopedTypeVariables -ddump-types -XTypeFamilies -XNoMonomorphismRestriction #-}
module Demo (demo, demo2) where
{-# OPTIONS_GHC -XModalTypes -dcore-lint -XScopedTypeVariables -ddump-types -XTypeFamilies -XNoMonomorphismRestriction #-}
module Demo (demo, demo2) where
+{-
+demo ::
+ <[ \input ->
+ let delayed = ~~reg output
+ output = ~~xor input delayed
+ in output ]>
+-}
+
demo z = <[ \y -> ~~z ]>
demo2 :: <[ (a,b) ~~> c ]>@d -> <[ () ~~> a ]>@d -> <[ b ~~>c ]>@d
demo z = <[ \y -> ~~z ]>
demo2 :: <[ (a,b) ~~> c ]>@d -> <[ () ~~> a ]>@d -> <[ b ~~>c ]>@d
@@
-85,4
+93,4
@@
sha256round =
k_plus_w)
t2 = adder s0 (maj3 a b c)
in h
k_plus_w)
t2 = adder s0 (maj3 a b c)
in h
- ]>
\ No newline at end of file
+ ]>