From: Adam Megacz Date: Fri, 27 May 2011 05:47:16 +0000 (-0700) Subject: update Demo.hs X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=a45824c7d03fcf797e22d2919187a7e97fb567cc update Demo.hs --- diff --git a/examples/Demo.hs b/examples/Demo.hs index afedde6..4c53aa5 100644 --- a/examples/Demo.hs +++ b/examples/Demo.hs @@ -1,15 +1,21 @@ {-# OPTIONS_GHC -XModalTypes -fcoqpass -dcore-lint #-} module Demo (demo) where + --demo con mer = <[ ~~mer ~~(con (2::Int)) ~~(con (12::Int)) ]> --- demo const mult = <[ let q = ~~(const (1::Int)) in ~~mult q q ]> +demo const mult = + <[ let twelve = ~~(const (12::Int)) + four = ~~(const ( 4::Int)) + in ~~mult four (~~mult four twelve) + ]> +{- demo const mult = <[ let twelve = ~~(const (12::Int)) in let four = ~~(const (4::Int)) in ~~mult four twelve ]> - +-} {- demo const mult = <[ let twelve = ~~(const (12::Int))