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:

All_Syntax
CSV
Compose
Constraints
Delta
Demo
Denormalize
Employees
FinanceColim1
FinanceColim2
ForeignKeys
Inverse
Joinless
LambdaConf
Linkage
Meta
OuterJoin
Petri
PharmaColim1
PharmaColim2
Pullback
Pushout
Query
QueryED
Quotient
Sigma
Tutorial
TutorialTSP
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
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