Safe Haskell	Trustworthy
Language	Haskell2010

Copilot.Theorem.Prover.SMT

Contents

Backends
Tactics
Auxiliary

Description

Connections to various SMT solvers and theorem provers.

Synopsis

data Backend a
class Show a => SmtFormat a
data SmtLib
data Tptp
yices :: Backend SmtLib
dReal :: Backend SmtLib
altErgo :: Backend SmtLib
metit :: String -> Backend Tptp
z3 :: Backend SmtLib
cvc4 :: Backend SmtLib
mathsat :: Backend SmtLib
data Options = Options {
- startK :: Word32
- maxK :: Word32
- debug :: Bool
}
induction :: SmtFormat a => Options -> Backend a -> Proof Universal
kInduction :: SmtFormat a => Options -> Backend a -> Proof Universal
onlySat :: SmtFormat a => Options -> Backend a -> Proof Existential
onlyValidity :: SmtFormat a => Options -> Backend a -> Proof Universal
class Default a where
- def :: a

Backends

data Backend a Source #

Backend to an SMT solver or theorem prover.

class Show a => SmtFormat a Source #

Format of SMT-Lib commands.

Minimal complete definition

push, pop, checkSat, setLogic, declFun, assert

Instances

Instances details

SmtFormat SmtLib Source #	Interface for SMT-Lib conforming backends.
Instance details Defined in Copilot.Theorem.Prover.SMTLib Methods push :: SmtLib pop :: SmtLib checkSat :: SmtLib setLogic :: String -> SmtLib declFun :: String -> Type -> [Type] -> SmtLib assert :: Expr -> SmtLib
SmtFormat Tptp Source #
Instance details Defined in Copilot.Theorem.Prover.TPTP Methods push :: Tptp pop :: Tptp checkSat :: Tptp setLogic :: String -> Tptp declFun :: String -> Type -> [Type] -> Tptp assert :: Expr -> Tptp

data SmtLib Source #

Type used to represent SMT-lib commands.

Use the interface in SmtFormat to create such commands.

Instances

Instances details

Show SmtLib Source #
Instance details Defined in Copilot.Theorem.Prover.SMTLib Methods showsPrec :: Int -> SmtLib -> ShowS # show :: SmtLib -> String # showList :: [SmtLib] -> ShowS #
SmtFormat SmtLib Source #	Interface for SMT-Lib conforming backends.
Instance details Defined in Copilot.Theorem.Prover.SMTLib Methods push :: SmtLib pop :: SmtLib checkSat :: SmtLib setLogic :: String -> SmtLib declFun :: String -> Type -> [Type] -> SmtLib assert :: Expr -> SmtLib

data Tptp Source #

Type used to represent TPTP expressions.

Although this type implements the SmtFormat interface, only assert is actually used.

Instances

Instances details

Show Tptp Source #
Instance details Defined in Copilot.Theorem.Prover.TPTP Methods showsPrec :: Int -> Tptp -> ShowS # show :: Tptp -> String # showList :: [Tptp] -> ShowS #
SmtFormat Tptp Source #
Instance details Defined in Copilot.Theorem.Prover.TPTP Methods push :: Tptp pop :: Tptp checkSat :: Tptp setLogic :: String -> Tptp declFun :: String -> Type -> [Type] -> Tptp assert :: Expr -> Tptp

yices :: Backend SmtLib Source #

Backend to the Yices 2 SMT solver.

It enables non-linear arithmetic (QF_NRA), which means MCSat will be used.

The command yices-smt2 must be in the user's PATH.

dReal :: Backend SmtLib Source #

Backend to the dReal SMT solver.

It enables non-linear arithmetic (QF_NRA).

The libraries for dReal must be installed and perl must be in the user's PATH.

altErgo :: Backend SmtLib Source #

Backend to the Alt-Ergo SMT solver.

It enables support for uninterpreted functions and mixed nonlinear arithmetic (QF_NIRA).

The command alt-ergo.opt must be in the user's PATH.

metit :: String -> Backend Tptp Source #

Backend to the MetiTaski theorem prover.

The command metit must be in the user's PATH.

The argument string is the path to the tptp subdirectory of the metitarski install location.

z3 :: Backend SmtLib Source #

Backend to the Z3 theorem prover.

The command z3 must be in the user's PATH.

cvc4 :: Backend SmtLib Source #

Backend to the cvc4 SMT solver.

It enables support for uninterpreted functions and mixed nonlinear arithmetic (QF_NIRA).

The command cvc4 must be in the user's PATH.

mathsat :: Backend SmtLib Source #

Backend to the Mathsat SMT solver.

It enables non-linear arithmetic (QF_NRA).

The command mathsat must be in the user's PATH.

Tactics

data Options Source #

Options to configure the provers.

Constructors

Options
Fields startK :: Word32 Initial `k` for the k-induction algorithm. maxK :: Word32 The maximum number of steps of the k-induction algorithm the prover runs before giving up. debug :: Bool If `debug` is set to `True`, the SMTLib/TPTP queries produced by the prover are displayed in the standard output.

Instances

Instances details

Default Options Source #	Default `Options` with a `0` `k` and a max of `10` steps, and that produce no debugging info.
Instance details Defined in Copilot.Theorem.Prover.SMT Methods def :: Options #

induction :: SmtFormat a => Options -> Backend a -> Proof Universal Source #

Tactic to find a proof by standard 1-induction.

The values for startK and maxK in the options are ignored.

kInduction :: SmtFormat a => Options -> Backend a -> Proof Universal Source #

Tactic to find a proof by k-induction.

onlySat :: SmtFormat a => Options -> Backend a -> Proof Existential Source #

Tactic to find only a proof of satisfiability.

onlyValidity :: SmtFormat a => Options -> Backend a -> Proof Universal Source #

Tactic to find only a proof of validity.

Auxiliary

class Default a where #

A class for types with a default value.

Minimal complete definition

Nothing

Methods

def :: a #

The default value for this type.

Instances

Instances details

Default All
Instance details Defined in Data.Default.Internal Methods def :: All #
Default Any
Instance details Defined in Data.Default.Internal Methods def :: Any #
Default CBool
Instance details Defined in Data.Default.Internal Methods def :: CBool #
Default CClock
Instance details Defined in Data.Default.Internal Methods def :: CClock #
Default CDouble
Instance details Defined in Data.Default.Internal Methods def :: CDouble #
Default CFloat
Instance details Defined in Data.Default.Internal Methods def :: CFloat #
Default CInt
Instance details Defined in Data.Default.Internal Methods def :: CInt #
Default CIntMax
Instance details Defined in Data.Default.Internal Methods def :: CIntMax #
Default CIntPtr
Instance details Defined in Data.Default.Internal Methods def :: CIntPtr #
Default CLLong
Instance details Defined in Data.Default.Internal Methods def :: CLLong #
Default CLong
Instance details Defined in Data.Default.Internal Methods def :: CLong #
Default CPtrdiff
Instance details Defined in Data.Default.Internal Methods def :: CPtrdiff #
Default CSUSeconds
Instance details Defined in Data.Default.Internal Methods def :: CSUSeconds #
Default CShort
Instance details Defined in Data.Default.Internal Methods def :: CShort #
Default CSigAtomic
Instance details Defined in Data.Default.Internal Methods def :: CSigAtomic #
Default CSize
Instance details Defined in Data.Default.Internal Methods def :: CSize #
Default CTime
Instance details Defined in Data.Default.Internal Methods def :: CTime #
Default CUInt
Instance details Defined in Data.Default.Internal Methods def :: CUInt #
Default CUIntMax
Instance details Defined in Data.Default.Internal Methods def :: CUIntMax #
Default CUIntPtr
Instance details Defined in Data.Default.Internal Methods def :: CUIntPtr #
Default CULLong
Instance details Defined in Data.Default.Internal Methods def :: CULLong #
Default CULong
Instance details Defined in Data.Default.Internal Methods def :: CULong #
Default CUSeconds
Instance details Defined in Data.Default.Internal Methods def :: CUSeconds #
Default CUShort
Instance details Defined in Data.Default.Internal Methods def :: CUShort #
Default IntPtr
Instance details Defined in Data.Default.Internal Methods def :: IntPtr #
Default WordPtr
Instance details Defined in Data.Default.Internal Methods def :: WordPtr #
Default Int16
Instance details Defined in Data.Default.Internal Methods def :: Int16 #
Default Int32
Instance details Defined in Data.Default.Internal Methods def :: Int32 #
Default Int64
Instance details Defined in Data.Default.Internal Methods def :: Int64 #
Default Int8
Instance details Defined in Data.Default.Internal Methods def :: Int8 #
Default Word16
Instance details Defined in Data.Default.Internal Methods def :: Word16 #
Default Word32
Instance details Defined in Data.Default.Internal Methods def :: Word32 #
Default Word64
Instance details Defined in Data.Default.Internal Methods def :: Word64 #
Default Word8
Instance details Defined in Data.Default.Internal Methods def :: Word8 #
Default IntSet
Instance details Defined in Data.Default.Internal Methods def :: IntSet #
Default Options Source #	Default options with unlimited unrolling for base and step.
Instance details Defined in Copilot.Theorem.Kind2.Prover Methods def :: Options #
Default Options Source #	Default `Options` with a `0` `k` and a max of `10` steps, and that produce no debugging info.
Instance details Defined in Copilot.Theorem.Prover.SMT Methods def :: Options #
Default Ordering
Instance details Defined in Data.Default.Internal Methods def :: Ordering #
Default Integer
Instance details Defined in Data.Default.Internal Methods def :: Integer #
Default ()
Instance details Defined in Data.Default.Internal Methods def :: () #
Default Bool
Instance details Defined in Data.Default.Internal Methods def :: Bool #
Default Double
Instance details Defined in Data.Default.Internal Methods def :: Double #
Default Float
Instance details Defined in Data.Default.Internal Methods def :: Float #
Default Int
Instance details Defined in Data.Default.Internal Methods def :: Int #
Default Word
Instance details Defined in Data.Default.Internal Methods def :: Word #
(Default a, RealFloat a) => Default (Complex a)
Instance details Defined in Data.Default.Internal Methods def :: Complex a #
Default a => Default (Identity a)
Instance details Defined in Data.Default.Internal Methods def :: Identity a #
Default (First a)
Instance details Defined in Data.Default.Internal Methods def :: First a #
Default (Last a)
Instance details Defined in Data.Default.Internal Methods def :: Last a #
Default a => Default (Dual a)
Instance details Defined in Data.Default.Internal Methods def :: Dual a #
Default (Endo a)
Instance details Defined in Data.Default.Internal Methods def :: Endo a #
Num a => Default (Product a)
Instance details Defined in Data.Default.Internal Methods def :: Product a #
Num a => Default (Sum a)
Instance details Defined in Data.Default.Internal Methods def :: Sum a #
Default (ConstPtr a)
Instance details Defined in Data.Default.Internal Methods def :: ConstPtr a #
Default (FunPtr a)
Instance details Defined in Data.Default.Internal Methods def :: FunPtr a #
Default (Ptr a)
Instance details Defined in Data.Default.Internal Methods def :: Ptr a #
Integral a => Default (Ratio a)
Instance details Defined in Data.Default.Internal Methods def :: Ratio a #
Default (IntMap v)
Instance details Defined in Data.Default.Internal Methods def :: IntMap v #
Default (Seq a)
Instance details Defined in Data.Default.Internal Methods def :: Seq a #
Default (Set v)
Instance details Defined in Data.Default.Internal Methods def :: Set v #
Default a => Default (Tree a)
Instance details Defined in Data.Default.Internal Methods def :: Tree a #
Default (Maybe a)
Instance details Defined in Data.Default.Internal Methods def :: Maybe a #
Default a => Default (a)
Instance details Defined in Data.Default.Internal Methods def :: (a) #
Default [a]
Instance details Defined in Data.Default.Internal Methods def :: [a] #
HasResolution a => Default (Fixed a)
Instance details Defined in Data.Default.Internal Methods def :: Fixed a #
Default (Proxy a)
Instance details Defined in Data.Default.Internal Methods def :: Proxy a #
Default (Map k v)
Instance details Defined in Data.Default.Internal Methods def :: Map k v #
(Default a1, Default a2) => Default (a1, a2)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2) #
Default a => Default (Const a b)
Instance details Defined in Data.Default.Internal Methods def :: Const a b #
(Default a1, Default a2, Default a3) => Default (a1, a2, a3)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3) #
(Default a1, Default a2, Default a3, Default a4) => Default (a1, a2, a3, a4)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3, a4) #
(Default a1, Default a2, Default a3, Default a4, Default a5) => Default (a1, a2, a3, a4, a5)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3, a4, a5) #
(Default a1, Default a2, Default a3, Default a4, Default a5, Default a6) => Default (a1, a2, a3, a4, a5, a6)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3, a4, a5, a6) #
(Default a1, Default a2, Default a3, Default a4, Default a5, Default a6, Default a7) => Default (a1, a2, a3, a4, a5, a6, a7)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3, a4, a5, a6, a7) #
(Default a1, Default a2, Default a3, Default a4, Default a5, Default a6, Default a7, Default a8) => Default (a1, a2, a3, a4, a5, a6, a7, a8)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3, a4, a5, a6, a7, a8) #
(Default a1, Default a2, Default a3, Default a4, Default a5, Default a6, Default a7, Default a8, Default a9) => Default (a1, a2, a3, a4, a5, a6, a7, a8, a9)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3, a4, a5, a6, a7, a8, a9) #
(Default a1, Default a2, Default a3, Default a4, Default a5, Default a6, Default a7, Default a8, Default a9, Default a10) => Default (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) #
(Default a1, Default a2, Default a3, Default a4, Default a5, Default a6, Default a7, Default a8, Default a9, Default a10, Default a11) => Default (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) #
(Default a1, Default a2, Default a3, Default a4, Default a5, Default a6, Default a7, Default a8, Default a9, Default a10, Default a11, Default a12) => Default (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) #
(Default a1, Default a2, Default a3, Default a4, Default a5, Default a6, Default a7, Default a8, Default a9, Default a10, Default a11, Default a12, Default a13) => Default (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) #
(Default a1, Default a2, Default a3, Default a4, Default a5, Default a6, Default a7, Default a8, Default a9, Default a10, Default a11, Default a12, Default a13, Default a14) => Default (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) #
(Default a1, Default a2, Default a3, Default a4, Default a5, Default a6, Default a7, Default a8, Default a9, Default a10, Default a11, Default a12, Default a13, Default a14, Default a15) => Default (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) #
(Default a1, Default a2, Default a3, Default a4, Default a5, Default a6, Default a7, Default a8, Default a9, Default a10, Default a11, Default a12, Default a13, Default a14, Default a15, Default a16) => Default (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16) #
(Default a1, Default a2, Default a3, Default a4, Default a5, Default a6, Default a7, Default a8, Default a9, Default a10, Default a11, Default a12, Default a13, Default a14, Default a15, Default a16, Default a17) => Default (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17) #
(Default a1, Default a2, Default a3, Default a4, Default a5, Default a6, Default a7, Default a8, Default a9, Default a10, Default a11, Default a12, Default a13, Default a14, Default a15, Default a16, Default a17, Default a18) => Default (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18) #
(Default a1, Default a2, Default a3, Default a4, Default a5, Default a6, Default a7, Default a8, Default a9, Default a10, Default a11, Default a12, Default a13, Default a14, Default a15, Default a16, Default a17, Default a18, Default a19) => Default (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19) #
(Default a1, Default a2, Default a3, Default a4, Default a5, Default a6, Default a7, Default a8, Default a9, Default a10, Default a11, Default a12, Default a13, Default a14, Default a15, Default a16, Default a17, Default a18, Default a19, Default a20) => Default (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20) #
(Default a1, Default a2, Default a3, Default a4, Default a5, Default a6, Default a7, Default a8, Default a9, Default a10, Default a11, Default a12, Default a13, Default a14, Default a15, Default a16, Default a17, Default a18, Default a19, Default a20, Default a21) => Default (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21) #
(Default a1, Default a2, Default a3, Default a4, Default a5, Default a6, Default a7, Default a8, Default a9, Default a10, Default a11, Default a12, Default a13, Default a14, Default a15, Default a16, Default a17, Default a18, Default a19, Default a20, Default a21, Default a22) => Default (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22) #
(Default a1, Default a2, Default a3, Default a4, Default a5, Default a6, Default a7, Default a8, Default a9, Default a10, Default a11, Default a12, Default a13, Default a14, Default a15, Default a16, Default a17, Default a18, Default a19, Default a20, Default a21, Default a22, Default a23) => Default (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23) #
(Default a1, Default a2, Default a3, Default a4, Default a5, Default a6, Default a7, Default a8, Default a9, Default a10, Default a11, Default a12, Default a13, Default a14, Default a15, Default a16, Default a17, Default a18, Default a19, Default a20, Default a21, Default a22, Default a23, Default a24) => Default (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24) #
(Default a1, Default a2, Default a3, Default a4, Default a5, Default a6, Default a7, Default a8, Default a9, Default a10, Default a11, Default a12, Default a13, Default a14, Default a15, Default a16, Default a17, Default a18, Default a19, Default a20, Default a21, Default a22, Default a23, Default a24, Default a25) => Default (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25) #
(Default a1, Default a2, Default a3, Default a4, Default a5, Default a6, Default a7, Default a8, Default a9, Default a10, Default a11, Default a12, Default a13, Default a14, Default a15, Default a16, Default a17, Default a18, Default a19, Default a20, Default a21, Default a22, Default a23, Default a24, Default a25, Default a26) => Default (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26) #
(Default a1, Default a2, Default a3, Default a4, Default a5, Default a6, Default a7, Default a8, Default a9, Default a10, Default a11, Default a12, Default a13, Default a14, Default a15, Default a16, Default a17, Default a18, Default a19, Default a20, Default a21, Default a22, Default a23, Default a24, Default a25, Default a26, Default a27) => Default (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27) #
(Default a1, Default a2, Default a3, Default a4, Default a5, Default a6, Default a7, Default a8, Default a9, Default a10, Default a11, Default a12, Default a13, Default a14, Default a15, Default a16, Default a17, Default a18, Default a19, Default a20, Default a21, Default a22, Default a23, Default a24, Default a25, Default a26, Default a27, Default a28) => Default (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28) #
(Default a1, Default a2, Default a3, Default a4, Default a5, Default a6, Default a7, Default a8, Default a9, Default a10, Default a11, Default a12, Default a13, Default a14, Default a15, Default a16, Default a17, Default a18, Default a19, Default a20, Default a21, Default a22, Default a23, Default a24, Default a25, Default a26, Default a27, Default a28, Default a29) => Default (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29) #
(Default a1, Default a2, Default a3, Default a4, Default a5, Default a6, Default a7, Default a8, Default a9, Default a10, Default a11, Default a12, Default a13, Default a14, Default a15, Default a16, Default a17, Default a18, Default a19, Default a20, Default a21, Default a22, Default a23, Default a24, Default a25, Default a26, Default a27, Default a28, Default a29, Default a30) => Default (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30) #
(Default a1, Default a2, Default a3, Default a4, Default a5, Default a6, Default a7, Default a8, Default a9, Default a10, Default a11, Default a12, Default a13, Default a14, Default a15, Default a16, Default a17, Default a18, Default a19, Default a20, Default a21, Default a22, Default a23, Default a24, Default a25, Default a26, Default a27, Default a28, Default a29, Default a30, Default a31) => Default (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31)
Instance details Defined in Data.Default.Internal Methods def :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31) #