Idris2Doc : Stellar.SQL

Stellar.SQL

(source)
Definitions
record ValidQuery : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkValidQuery : (0 ty : Type) -> (tr : ToRow ty) -> (qy : Query ty) -> {auto 0 _ : ToRowTypes ty = FromRowTypes ty} -> ValidQuery

  Projections:
  
0 .chk : ({rec:0} : ValidQuery) -> ToRowTypes (ty {rec:0}) = FromRowTypes (ty {rec:0})
  
.qy : ({rec:0} : ValidQuery) -> Query (ty {rec:0})
  
.tr : ({rec:0} : ValidQuery) -> ToRow (ty {rec:0})
  
0 .ty : ValidQuery -> Type
0 .ty : ValidQuery -> Type
  Totality: total
  Visibility: public export
0 ty : ValidQuery -> Type
  Totality: total
  Visibility: public export
.tr : ({rec:0} : ValidQuery) -> ToRow (ty {rec:0})
  Totality: total
  Visibility: public export
tr : ({rec:0} : ValidQuery) -> ToRow (ty {rec:0})
  Totality: total
  Visibility: public export
.qy : ({rec:0} : ValidQuery) -> Query (ty {rec:0})
  Totality: total
  Visibility: public export
qy : ({rec:0} : ValidQuery) -> Query (ty {rec:0})
  Totality: total
  Visibility: public export
0 .chk : ({rec:0} : ValidQuery) -> ToRowTypes (ty {rec:0}) = FromRowTypes (ty {rec:0})
  Totality: total
  Visibility: public export
0 chk : ({rec:0} : ValidQuery) -> ToRowTypes (ty {rec:0}) = FromRowTypes (ty {rec:0})
  Totality: total
  Visibility: public export
runValid : Has SqlError e => DB => (x : ValidQuery) -> App e (Table (x .ty))
  Totality: total
  Visibility: export
0 Errs : List Type
  Totality: total
  Visibility: public export
0 SQLM : API -> API
  Totality: total
  Visibility: public export
DBCmd : API
  Totality: total
  Visibility: public export
0 DBQry : API
  Totality: total
  Visibility: public export
CmdCostate : DB => Costate (SQLM DBCmd)
  Totality: total
  Visibility: export
DBQueryCostate : DB => Costate (SQLM DBQry)
  Totality: total
  Visibility: export
0 SQL : API
  Totality: total
  Visibility: public export
DBCostate : DB => Costate (SQLM SQL)
  Totality: total
  Visibility: export
execSeqDB : DB => (x : (SQLM (SQL .star)) .message) -> (SQLM (SQL .star)) .response x
  Totality: total
  Visibility: export
DBStarCostate : DB => Costate (SQLM (SQL .star))
  Run any amount of DB queries wrapped in SQL errors

  Totality: total
  Visibility: export