examples/Demo.hs

   1 {-# OPTIONS_GHC -XModalTypes -fcoqpass -dcore-lint #-}
   2 module Demo (demo) where
   3
   4 --demo con mer = <[ ~~mer ~~(con (2::Int)) ~~(con (12::Int)) ]>
   5
   6 -- demo const mult = <[ let q = ~~(const (1::Int)) in ~~mult q q ]>
   7
   8 demo const mult =
   9  <[ let     twelve = ~~(const (12::Int))
  10     in let  four    = ~~(const (4::Int))
  11          in  ~~mult four twelve  ]>
  12
  13 {-
  14 demo const mult =
  15  <[ let     twelve = ~~(const (12::Int))
  16     in let  twelvea = twelve
  17             four    = ~~(const (4::Int))
  18             twelveb = twelve
  19          in  ~~mult (~~mult twelvea four) (~~mult twelveb twelveb) ]>
  20 -}
  21
  22 {-
  23 demo const mult = demo' 3
  24  where
  25   demo' 0 = const 12
  26   demo' 1 = const 12
  27   demo' n = <[ ~~mult ~~(demo' (n-1)) ~~(demo' (n-2)) ]>
  28 -}