X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=examples%2FDemo.hs;h=6d0e69ddd19f9d5208cc4b621919de33cc210d74;hp=afedde6d253f0a13aca99814ddcea27aa38ea9ec;hb=171beb27508a340b24ab14837e72451d0b500805;hpb=b83e779e742413ca84df565263dafbdf9f79920a diff --git a/examples/Demo.hs b/examples/Demo.hs index afedde6..6d0e69d 100644 --- a/examples/Demo.hs +++ b/examples/Demo.hs @@ -1,15 +1,21 @@ -{-# OPTIONS_GHC -XModalTypes -fcoqpass -dcore-lint #-} +{-# OPTIONS_GHC -XModalTypes -fflatten -funsafe-skolemize -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))