opaque Database.PostgreSQL.LibPQ.PgConnHandle : NonemptyType

Opaque PostgreSQL connection handle. $$\text{PgConn} : \text{NonemptyType}$$ Wraps libpq's PGconn*. The GC finalizer calls PQfinish.

def Database.PostgreSQL.LibPQ.PgConn : Type

A live (or formerly-live) PostgreSQL connection.

Equations

• Database.PostgreSQL.LibPQ.PgConn = Database.PostgreSQL.LibPQ.PgConnHandle.type

instance Database.PostgreSQL.LibPQ.instNonemptyPgConn : Nonempty PgConn

opaque Database.PostgreSQL.LibPQ.PgResultHandle : NonemptyType

Opaque PostgreSQL result handle. $$\text{PgResult} : \text{NonemptyType}$$ Wraps libpq's PGresult*. The GC finalizer calls PQclear.

def Database.PostgreSQL.LibPQ.PgResult : Type

A query result set.

Equations

• Database.PostgreSQL.LibPQ.PgResult = Database.PostgreSQL.LibPQ.PgResultHandle.type

instance Database.PostgreSQL.LibPQ.instNonemptyPgResult : Nonempty PgResult

inductive Database.PostgreSQL.LibPQ.ConnStatus : Type

Connection status returned by PQstatus. $$\text{ConnStatus} \in \{\text{ok}, \text{bad}, \text{other}\}$$

• ok : ConnStatus
• bad : ConnStatus
• other (code : UInt8) : ConnStatus

def Database.PostgreSQL.LibPQ.instBEqConnStatus.beq : ConnStatus → ConnStatus → Bool

Equations

• Database.PostgreSQL.LibPQ.instBEqConnStatus.beq Database.PostgreSQL.LibPQ.ConnStatus.ok Database.PostgreSQL.LibPQ.ConnStatus.ok = true
• Database.PostgreSQL.LibPQ.instBEqConnStatus.beq Database.PostgreSQL.LibPQ.ConnStatus.bad Database.PostgreSQL.LibPQ.ConnStatus.bad = true
• Database.PostgreSQL.LibPQ.instBEqConnStatus.beq (Database.PostgreSQL.LibPQ.ConnStatus.other a) (Database.PostgreSQL.LibPQ.ConnStatus.other b) = (a == b)
• Database.PostgreSQL.LibPQ.instBEqConnStatus.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Database.PostgreSQL.LibPQ.instBEqConnStatus : BEq ConnStatus

Equations

• Database.PostgreSQL.LibPQ.instBEqConnStatus = { beq := Database.PostgreSQL.LibPQ.instBEqConnStatus.beq }

def Database.PostgreSQL.LibPQ.instReprConnStatus.repr : ConnStatus → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Database.PostgreSQL.LibPQ.instReprConnStatus : Repr ConnStatus

Equations

• Database.PostgreSQL.LibPQ.instReprConnStatus = { reprPrec := Database.PostgreSQL.LibPQ.instReprConnStatus.repr }

@[implicit_reducible]

instance Database.PostgreSQL.LibPQ.instInhabitedConnStatus : Inhabited ConnStatus

Equations

• Database.PostgreSQL.LibPQ.instInhabitedConnStatus = { default := Database.PostgreSQL.LibPQ.instInhabitedConnStatus.default }

def Database.PostgreSQL.LibPQ.instInhabitedConnStatus.default : ConnStatus

Equations

• Database.PostgreSQL.LibPQ.instInhabitedConnStatus.default = Database.PostgreSQL.LibPQ.ConnStatus.ok

def Database.PostgreSQL.LibPQ.ConnStatus.ofUInt8 : UInt8 → ConnStatus

Decode a raw PQstatus integer into ConnStatus.

Equations

• Database.PostgreSQL.LibPQ.ConnStatus.ofUInt8 0 = Database.PostgreSQL.LibPQ.ConnStatus.ok
• Database.PostgreSQL.LibPQ.ConnStatus.ofUInt8 1 = Database.PostgreSQL.LibPQ.ConnStatus.bad
• Database.PostgreSQL.LibPQ.ConnStatus.ofUInt8 x✝ = Database.PostgreSQL.LibPQ.ConnStatus.other x✝

inductive Database.PostgreSQL.LibPQ.ExecStatus : Type

Result status returned by PQresultStatus. $$\text{ExecStatus} \in \{\text{emptyQuery}, \text{commandOk}, \ldots\}$$

• emptyQuery : ExecStatus
• commandOk : ExecStatus
• tuplesOk : ExecStatus
• copyOut : ExecStatus
• copyIn : ExecStatus
• badResponse : ExecStatus
• nonfatalError : ExecStatus
• fatalError : ExecStatus
• copyBoth : ExecStatus
• singleTuple : ExecStatus
• pipelineSync : ExecStatus
• pipelineAbort : ExecStatus
• other (code : UInt8) : ExecStatus

@[implicit_reducible]

instance Database.PostgreSQL.LibPQ.instBEqExecStatus : BEq ExecStatus

Equations

• Database.PostgreSQL.LibPQ.instBEqExecStatus = { beq := Database.PostgreSQL.LibPQ.instBEqExecStatus.beq }

def Database.PostgreSQL.LibPQ.instBEqExecStatus.beq : ExecStatus → ExecStatus → Bool

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Database.PostgreSQL.LibPQ.instReprExecStatus : Repr ExecStatus

Equations

• Database.PostgreSQL.LibPQ.instReprExecStatus = { reprPrec := Database.PostgreSQL.LibPQ.instReprExecStatus.repr }

def Database.PostgreSQL.LibPQ.instReprExecStatus.repr : ExecStatus → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Database.PostgreSQL.LibPQ.instInhabitedExecStatus.default : ExecStatus

Equations

• Database.PostgreSQL.LibPQ.instInhabitedExecStatus.default = Database.PostgreSQL.LibPQ.ExecStatus.emptyQuery

@[implicit_reducible]

instance Database.PostgreSQL.LibPQ.instInhabitedExecStatus : Inhabited ExecStatus

Equations

• Database.PostgreSQL.LibPQ.instInhabitedExecStatus = { default := Database.PostgreSQL.LibPQ.instInhabitedExecStatus.default }

def Database.PostgreSQL.LibPQ.ExecStatus.ofUInt8 : UInt8 → ExecStatus

Decode a raw PQresultStatus integer.

Equations

• Database.PostgreSQL.LibPQ.ExecStatus.ofUInt8 0 = Database.PostgreSQL.LibPQ.ExecStatus.emptyQuery
• Database.PostgreSQL.LibPQ.ExecStatus.ofUInt8 1 = Database.PostgreSQL.LibPQ.ExecStatus.commandOk
• Database.PostgreSQL.LibPQ.ExecStatus.ofUInt8 2 = Database.PostgreSQL.LibPQ.ExecStatus.tuplesOk
• Database.PostgreSQL.LibPQ.ExecStatus.ofUInt8 3 = Database.PostgreSQL.LibPQ.ExecStatus.copyOut
• Database.PostgreSQL.LibPQ.ExecStatus.ofUInt8 4 = Database.PostgreSQL.LibPQ.ExecStatus.copyIn
• Database.PostgreSQL.LibPQ.ExecStatus.ofUInt8 5 = Database.PostgreSQL.LibPQ.ExecStatus.badResponse
• Database.PostgreSQL.LibPQ.ExecStatus.ofUInt8 6 = Database.PostgreSQL.LibPQ.ExecStatus.nonfatalError
• Database.PostgreSQL.LibPQ.ExecStatus.ofUInt8 7 = Database.PostgreSQL.LibPQ.ExecStatus.fatalError
• Database.PostgreSQL.LibPQ.ExecStatus.ofUInt8 8 = Database.PostgreSQL.LibPQ.ExecStatus.copyBoth
• Database.PostgreSQL.LibPQ.ExecStatus.ofUInt8 9 = Database.PostgreSQL.LibPQ.ExecStatus.singleTuple
• Database.PostgreSQL.LibPQ.ExecStatus.ofUInt8 10 = Database.PostgreSQL.LibPQ.ExecStatus.pipelineSync
• Database.PostgreSQL.LibPQ.ExecStatus.ofUInt8 11 = Database.PostgreSQL.LibPQ.ExecStatus.pipelineAbort
• Database.PostgreSQL.LibPQ.ExecStatus.ofUInt8 x✝ = Database.PostgreSQL.LibPQ.ExecStatus.other x✝

def Database.PostgreSQL.LibPQ.ExecStatus.isOk : ExecStatus → Bool

Is this a successful exec status?

Equations

• Database.PostgreSQL.LibPQ.ExecStatus.commandOk.isOk = true
• Database.PostgreSQL.LibPQ.ExecStatus.tuplesOk.isOk = true
• Database.PostgreSQL.LibPQ.ExecStatus.singleTuple.isOk = true
• Database.PostgreSQL.LibPQ.ExecStatus.emptyQuery.isOk = true
• x✝.isOk = false

theorem Database.PostgreSQL.LibPQ.ExecStatus.commandOk_isOk : commandOk.isOk = true

theorem Database.PostgreSQL.LibPQ.ExecStatus.tuplesOk_isOk : tuplesOk.isOk = true

theorem Database.PostgreSQL.LibPQ.ExecStatus.singleTuple_isOk : singleTuple.isOk = true

theorem Database.PostgreSQL.LibPQ.ExecStatus.emptyQuery_isOk : emptyQuery.isOk = true

theorem Database.PostgreSQL.LibPQ.ExecStatus.badResponse_not_isOk : badResponse.isOk = false

theorem Database.PostgreSQL.LibPQ.ExecStatus.fatalError_not_isOk : fatalError.isOk = false

theorem Database.PostgreSQL.LibPQ.ExecStatus.nonfatalError_not_isOk : nonfatalError.isOk = false

inductive Database.PostgreSQL.LibPQ.TransactionStatus : Type

Transaction status returned by PQtransactionStatus.

• idle : TransactionStatus
• active : TransactionStatus
• inTrans : TransactionStatus
• inError : TransactionStatus
• unknown : TransactionStatus

def Database.PostgreSQL.LibPQ.instBEqTransactionStatus.beq : TransactionStatus → TransactionStatus → Bool

Equations

• Database.PostgreSQL.LibPQ.instBEqTransactionStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Database.PostgreSQL.LibPQ.instBEqTransactionStatus : BEq TransactionStatus

Equations

• Database.PostgreSQL.LibPQ.instBEqTransactionStatus = { beq := Database.PostgreSQL.LibPQ.instBEqTransactionStatus.beq }

def Database.PostgreSQL.LibPQ.instReprTransactionStatus.repr : TransactionStatus → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Database.PostgreSQL.LibPQ.instReprTransactionStatus : Repr TransactionStatus

Equations

• Database.PostgreSQL.LibPQ.instReprTransactionStatus = { reprPrec := Database.PostgreSQL.LibPQ.instReprTransactionStatus.repr }

@[implicit_reducible]

instance Database.PostgreSQL.LibPQ.instInhabitedTransactionStatus : Inhabited TransactionStatus

Equations

• Database.PostgreSQL.LibPQ.instInhabitedTransactionStatus = { default := Database.PostgreSQL.LibPQ.instInhabitedTransactionStatus.default }

def Database.PostgreSQL.LibPQ.instInhabitedTransactionStatus.default : TransactionStatus

Equations

• Database.PostgreSQL.LibPQ.instInhabitedTransactionStatus.default = Database.PostgreSQL.LibPQ.TransactionStatus.idle

def Database.PostgreSQL.LibPQ.TransactionStatus.ofUInt8 : UInt8 → TransactionStatus

Decode raw transaction status.

Equations

• Database.PostgreSQL.LibPQ.TransactionStatus.ofUInt8 0 = Database.PostgreSQL.LibPQ.TransactionStatus.idle
• Database.PostgreSQL.LibPQ.TransactionStatus.ofUInt8 1 = Database.PostgreSQL.LibPQ.TransactionStatus.active
• Database.PostgreSQL.LibPQ.TransactionStatus.ofUInt8 2 = Database.PostgreSQL.LibPQ.TransactionStatus.inTrans
• Database.PostgreSQL.LibPQ.TransactionStatus.ofUInt8 3 = Database.PostgreSQL.LibPQ.TransactionStatus.inError
• Database.PostgreSQL.LibPQ.TransactionStatus.ofUInt8 x✝ = Database.PostgreSQL.LibPQ.TransactionStatus.unknown

structure Database.PostgreSQL.LibPQ.PgError : Type

A PostgreSQL error returned from libpq.

• message : String
• status : ExecStatus

def Database.PostgreSQL.LibPQ.instBEqPgError.beq : PgError → PgError → Bool

Equations

• Database.PostgreSQL.LibPQ.instBEqPgError.beq { message := a, status := a_1 } { message := b, status := b_1 } = (a == b && a_1 == b_1)
• Database.PostgreSQL.LibPQ.instBEqPgError.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Database.PostgreSQL.LibPQ.instBEqPgError : BEq PgError

Equations

• Database.PostgreSQL.LibPQ.instBEqPgError = { beq := Database.PostgreSQL.LibPQ.instBEqPgError.beq }

def Database.PostgreSQL.LibPQ.instReprPgError.repr : PgError → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Database.PostgreSQL.LibPQ.instReprPgError : Repr PgError

Equations

• Database.PostgreSQL.LibPQ.instReprPgError = { reprPrec := Database.PostgreSQL.LibPQ.instReprPgError.repr }

@[implicit_reducible]

instance Database.PostgreSQL.LibPQ.instToStringPgError : ToString PgError

Equations

• One or more equations did not get rendered due to their size.

structure Database.PostgreSQL.LibPQ.PgNotification : Type

A LISTEN/NOTIFY notification from PostgreSQL.

• channel : String
• payload : String
• pid : UInt32

def Database.PostgreSQL.LibPQ.instBEqPgNotification.beq : PgNotification → PgNotification → Bool

Equations

• Database.PostgreSQL.LibPQ.instBEqPgNotification.beq { channel := a, payload := a_1, pid := a_2 } { channel := b, payload := b_1, pid := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Database.PostgreSQL.LibPQ.instBEqPgNotification.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Database.PostgreSQL.LibPQ.instBEqPgNotification : BEq PgNotification

Equations

• Database.PostgreSQL.LibPQ.instBEqPgNotification = { beq := Database.PostgreSQL.LibPQ.instBEqPgNotification.beq }

def Database.PostgreSQL.LibPQ.instReprPgNotification.repr : PgNotification → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Database.PostgreSQL.LibPQ.instReprPgNotification : Repr PgNotification

Equations

• Database.PostgreSQL.LibPQ.instReprPgNotification = { reprPrec := Database.PostgreSQL.LibPQ.instReprPgNotification.repr }