Copilot.Language.Spec

Copilot specifications.

Documentation

type Spec = Writer [SpecItem] ()

type Spec' a = Writer [SpecItem] a

runSpec :: Spec' a -> [SpecItem]

data SpecItem

data Observer where

Constructors

Observer :: Typed a => String -> Stream a -> Observer

observer :: Typed a => String -> Stream a -> Spec

observers :: [SpecItem] -> [Observer]

data Trigger where

Constructors

Trigger :: Name -> Stream Bool -> [Arg] -> Trigger

trigger :: String -> Stream Bool -> [Arg] -> Spec

triggers :: [SpecItem] -> [Trigger]

arg :: Typed a => Stream a -> Arg

data Property where

Constructors

Property :: String -> Stream Bool -> Property

data Prop a where

Constructors

Forall :: Stream Bool -> Prop Universal

Exists :: Stream Bool -> Prop Existential

prop :: String -> Prop a -> Writer [SpecItem] (PropRef a)

properties :: [SpecItem] -> [Property]

theorem :: String -> Prop a -> Proof a -> Writer [SpecItem] (PropRef a)

theorems :: [SpecItem] -> [(Property, UProof)]

forall :: Stream Bool -> Prop Universal

exists :: Stream Bool -> Prop Existential

extractProp :: Prop a -> Stream Bool

data Universal

data Existential