use CoreM monad to acquire known-to-compiler identifiers

[coq-hetmet.git] / examples / Demo.hs

diff --git a/examples/Demo.hs b/examples/Demo.hs
index bac14ab..0a5e4e4 100644 (file)
--- a/examples/Demo.hs
+++ b/examples/Demo.hs
@@ -2,10 +2,21 @@
 module Demo (demo) where
 
 
---demo const mult = <[ \(y::Int) -> ~~mult y ~~(const 12) ]>
+demo const mult = <[ \(y::Int) -> ~~mult y ~~(const 12) ]>
+{-
+demo const mult = <[ \y -> ~~(demo' 0) ]>
+  where
+   demo' 0 = const 4
+   demo' n = const 4
+-}
+-- demo' n = <[ ~~mult ~~(demo' (n-1)) ~~(demo' (n-1)) ]>
+
 
+
+{-
 demo const mult =
    <[ \y -> let y = ~~(const 4) in ~~mult (~~mult y y) (~~mult y y) ]>
+-}
 
 {-
 demo const mult =