constraints constraints_literal

typeside t
schema s : t
----------------------------------
constraints (literal : s {}) : s

A set of data integrity constraints, i.e., a theory in regular logic or a set of embedded dependencies (EDs), or finite limit logic plus epis. Each constraint is also a transform; satisfying it is tantamount to solving a lifting problem. See All_Syntax for an example. Note that you can write 'exists unique'.

Appears in:

All_Syntax
CQL_def
Constraints
Demo
FOAF
LambdaConf
Meta
NewDemo
NewDemoPsuedo
PartialOrder
Petri
PointsTo
Pullback
QueryED
vsSQL3

Options:

allow_empty_sorts_unsafe
always_reload
completion_compose
completion_filter_subsumed
completion_precedence
completion_sort
completion_syntactic_ac
completion_unfailing
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
second_prover
talg_reduction
timeout
triviality_check_best_effort
vampire_path