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:

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