typeside t schema s : t ---------------------------------- instance (literal : s {}) : sA 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 aliceis equivalent to

equations person1.name = bill person2.name = aliceThe 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