Language.Hasmtlib.Lens

Documentation

somePlate :: forall t f. (KnownSMTSort t, Applicative f) => (Expr t -> f (Expr t)) -> forall s. KnownSMTSort s => Expr s -> f (Expr s)

Apply the plate-function f for given Expr expr if possible. Otherwise try to apply f for the children of expr. **Caution for quantified expressions:** 'plate-function' f will only be applied if quantification already has taken place.(&&) Therefore make sure quantify has been run before. Otherwise the quantified expression and therefore all it's sub-expressions will not have f applied.

Orphan instances

(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Ixed (Expr ('ArraySort k v))

Methods

ix :: Index (Expr ('ArraySort k v)) -> Traversal' (Expr ('ArraySort k v)) (IxValue (Expr ('ArraySort k v)))

Ixed (Expr 'StringSort)

Methods

ix :: Index (Expr 'StringSort) -> Traversal' (Expr 'StringSort) (IxValue (Expr 'StringSort))

AsEmpty (Expr 'StringSort)

Methods

_Empty :: Prism' (Expr 'StringSort) ()

KnownSMTSort t => Plated (Expr t)

• *Caution for quantified expressions:** 'plate-function' f will only be applied if quantification already has taken place.(&&) Therefore make sure quantify has been run before. Otherwise the quantified expression and therefore all it's sub-expressions will not have f applied.

Methods

plate :: Traversal' (Expr t) (Expr t)

Prefixed (Expr 'StringSort)

Methods

prefixed :: Expr 'StringSort -> Prism' (Expr 'StringSort) (Expr 'StringSort)

Suffixed (Expr 'StringSort)

Methods

suffixed :: Expr 'StringSort -> Prism' (Expr 'StringSort) (Expr 'StringSort)

Cons (Expr 'StringSort) (Expr 'StringSort) (Expr 'StringSort) (Expr 'StringSort)

Methods

_Cons :: Prism (Expr 'StringSort) (Expr 'StringSort) (Expr 'StringSort, Expr 'StringSort) (Expr 'StringSort, Expr 'StringSort)

Snoc (Expr 'StringSort) (Expr 'StringSort) (Expr 'StringSort) (Expr 'StringSort)

Methods

_Snoc :: Prism (Expr 'StringSort) (Expr 'StringSort) (Expr 'StringSort, Expr 'StringSort) (Expr 'StringSort, Expr 'StringSort)