query query_literal

typeside t
schema s1 : t
schema s2 : t
----------------------------------
query (literal : s1 -> s2 {}) : s1 -> s2

A query literal, known informally as an uber-flower. Equivalent to a co-span of mapping, and generalizes relational conjunctive queries to multiple target tables with foreign keys. If Q is from S to T, then for each entity t in T we have a from where query or so-called frozen S instance Q(t). Furthermore, for each foreign key fk taking e1 to e2 Q(fk) is a tranform from Q(e2) to Q(e1), i.e., contravariantly. Similarly, each attribute att from e to t has a corresponding transform Q(att) from the representable instance y_t to Q(e). See All_Syntax for an example.

Appears in:

Aggregation
All_Syntax
Compose
Dataversity
Demo
FinanceColim1
ForeignKeys
JDBCSQL
Joinless
LambdaConf
OuterJoin
Pullback
Pushout
Query
QueryED
RExt
Tutorial
UnitConv
vsSQL1

Options:

allow_empty_sorts_unsafe
always_reload
completion_compose
completion_filter_subsumed
completion_precedence
completion_sort
completion_syntactic_ac
completion_unfailing
dont_validate_unsafe
dont_verify_is_appropriate_for_prover_unsafe
e_path
e_use_auto
maedmax_path
num_threads
program_allow_nonconfluence_unsafe
program_allow_nontermination_unsafe
prover
prover_simplify_max
query_remove_redundancy
second_prover
talg_reduction
timeout
triviality_check_best_effort
vampire_path