instance instance_literal

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

A literal instance, given by generating rows and labelled nulls, and ground equations. As always, quotes can be used; for example, to write negative numbers. Convient additional syntax:

multi_equations
	name -> person1 bill, person2 alice

is equivalent to

equations
	person1.name = bill
	person2.name = alice

The key-value pairs in multi-equations must be comma separated (necessary for readability and error correction). See require_consistency, and interpret_as_algebra, which interprets the instance as a model, similar to JDBC / CSV import. This behavior can be useful when writing down an instance that is already saturated and for which one wants to check the schema constraints, rather than impose them. See All_Syntax for an example.

Appears in:

Aggregation
All_Syntax
Compose
Constraints
Dataversity
Delta
Demo
Denormalize
Employees
FinanceColim1
ForeignKeys
Inverse
Joinless
LambdaConf
Linkage
Meta
NewDemo
NewDemoPsuedo
OuterJoin
PartialOrder
Petri
PharmaColim1
PharmaColim2
PointsTo
Pullback
Pushout
Query
QueryED
Quotient
RDF Jena
RExt
Sigma
Spans
Tutorial
UnitConv
vsSQL1
vsSQL2
vsSQL3

Options:

allow_empty_sorts_unsafe
allow_java_eqs_unsafe
always_reload
completion_compose
completion_filter_subsumed
completion_precedence
completion_sort
completion_syntactic_ac
completion_unfailing
diverge_limit
diverge_warn
dont_verify_is_appropriate_for_prover_unsafe
e_path
e_use_auto
import_dont_check_closure_unsafe
interpret_as_algebra
maedmax_path
num_threads
program_allow_nonconfluence_unsafe
program_allow_nontermination_unsafe
prover
prover_simplify_max
require_consistency
second_prover
talg_reduction
timeout
triviality_check_best_effort
vampire_path