ListDataCons.hs

module Fixme where


{-@ hsig :: x:a -> {v:[a] | v == (x:[])} @-} 
hsig :: a -> [a] 
hsig x = [x] 


{-

This crashes with 

(VV#F1 = fix#GHC.Types.#58##35#64([x#aJP; fix#GHC.Types.#91##93##35#6m([])]))

z3Pred: error converting (VV#F1 = fix#GHC.Types.#58##35#64([x#aJP; fix#GHC.Types.#91##93##35#6m([])]))
Fatal error: exception Failure("bracket hits exn: TpGen.MakeProver(SMT).Z3RelTypeError
")

Unless these edits

https://github.com/ucsd-progsys/liquid-fixpoint/commit/63e1e1ccfbde4d7a26bd3e328ad111423172a7e9


-}