sbv-8.1: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Data.SBV.Tuple

Description

Accessing symbolic tuple fields and deconstruction.

Synopsis

# Symbolic field access

(^.) :: a -> (a -> b) -> b infixl 8 Source #

Field access, inspired by the lens library. This is merely reverse application, but allows us to write things like (1, 2)^._1 which is likely to be familiar to most Haskell programmers out there. Note that this is precisely equivalent to _1 (1, 2), but perhaps it reads a little nicer.

_1 :: HasField "_1" b a => SBV a -> SBV b Source #

Access the 1st element of an STupleN, 2 <= N <= 8. Also see ^..

_2 :: HasField "_2" b a => SBV a -> SBV b Source #

Access the 2nd element of an STupleN, 2 <= N <= 8. Also see ^..

_3 :: HasField "_3" b a => SBV a -> SBV b Source #

Access the 3nd element of an STupleN, 3 <= N <= 8. Also see ^..

_4 :: HasField "_4" b a => SBV a -> SBV b Source #

Access the 4th element of an STupleN, 4 <= N <= 8. Also see ^..

_5 :: HasField "_5" b a => SBV a -> SBV b Source #

Access the 5th element of an STupleN, 5 <= N <= 8. Also see ^..

_6 :: HasField "_6" b a => SBV a -> SBV b Source #

Access the 6th element of an STupleN, 6 <= N <= 8. Also see ^..

_7 :: HasField "_7" b a => SBV a -> SBV b Source #

Access the 7th element of an STupleN, 7 <= N <= 8. Also see ^..

_8 :: HasField "_8" b a => SBV a -> SBV b Source #

Access the 8th element of an STupleN, 8 <= N <= 8. Also see ^..

# Tupling and untupling

tuple :: Tuple tup a => a -> SBV tup Source #

Constructing a tuple from its parts. Forms an isomorphism pair with tuple:

>>> prove $\p -> untuple @(Integer, Bool, (String, Char)) (tuple p) .== p Q.E.D.  untuple :: Tuple tup a => SBV tup -> a Source # Deconstruct a tuple, getting its constituent parts apart. Forms an isomorphism pair with untuple: >>> prove$ \p -> tuple @(Integer, Bool, (String, Char)) (untuple p) .== p
Q.E.D.