Glossary

Every keyword, operator, type, directive and annotation in L4, with a one-line meaning and a link to the page that describes it. Functions are listed under Built-in functions and Standard libraries.

Functions

Keyword	Meaning	Reference
DECIDE	Defines a value, a function or a rule; one definition or several clauses	DECIDE
MEANS	Gives the body of a function, a value or a computed field	MEANS
IS	Gives the body after `DECIDE name`; also states a type (`IS A NUMBER`)	DECIDE
IF (after DECIDE)	`DECIDE x IF condition` defines a BOOLEAN	DECIDE
GIVEN	Names and types the inputs of a function	GIVEN and GIVETH
GIVETH / GIVES	States the type of the result	GIVEN and GIVETH
LET ... IN	Local definitions before an expression	LET and WHERE
BE / MEAN	Alternatives to IS and MEANS in a LET binding	LET and WHERE
WHERE	Local definitions after an expression	LET and WHERE
YIELD	A function without a name: `GIVEN n YIELD n + 1`	YIELD
AKA	Another name for the same function, value, type or section	AKA
Several clauses	A rule written as one line per case: `DECIDE price Red IS 1`	DECIDE

Types

Keyword	Meaning	Reference
DECLARE	Defines a new type	DECLARE
HAS	Lists the fields of a record, including computed fields with MEANS	DECLARE
ONE OF	Lists the alternatives of an enumeration	DECLARE
IS A / IS AN	States a type: `age IS A NUMBER`	DECLARE
A / AN / THE	Articles before a type name; they do not change the meaning	DECLARE
OF	Applies a type or a constructor to its arguments: `LIST OF NUMBER`, `PAIR OF x, y`	DECLARE
WITH	Builds a record by field name: `Person WITH name IS "Ann"`	DECLARE
ASSUME	Declares a name with a type but no definition	ASSUME
TYPE	The type of types, for type inputs: `GIVEN a IS A TYPE`	FOR ALL
FOR ALL	Introduces type variables in a type	FOR ALL
FUNCTION FROM ... TO	A function type: `FUNCTION FROM NUMBER TO BOOLEAN`	Types
AS	`x AS STRING` turns a value into text	Coercions

Built-in types

Type	Meaning	Reference
NUMBER	Whole numbers and exact fractions	Types
STRING	Text	Types
BOOLEAN	`TRUE` or `FALSE`	Types
DATE	A calendar date	Types
TIME	A time of day, with no date or time zone	Types
DATETIME	A moment in time, with a time zone	Types
LIST	A list of values of one type; also writes a list: `LIST 1, 2, 3`	Types
MAYBE	A value that may be missing: `JUST x` or `NOTHING`	Types
EITHER	One of two values: `LEFT x` or `RIGHT y`	Types
PAIR	Two values together, from the prelude	prelude
Dictionary	Keys mapped to values, from the prelude	prelude
DEONTIC	The type of a regulative rule: `DEONTIC party action`	DEONTIC
PROVISION	An older name for DEONTIC	DEONTIC
EVENT	Something a party did at a time, for traces: `EVENT party action`	EVENT

Constants and constructors

Name	Meaning	Reference
TRUE / FALSE	The two BOOLEAN values	Types
JUST / NOTHING	A present or a missing MAYBE value	Types
LEFT / RIGHT	The two sides of an EITHER	Types
EMPTY	The empty list	Types
TODAY, NOW, CURRENTTIME, TIMEZONE	The current date, moment and time of day, and the document's time zone	Built-in functions

Control flow

Keyword	Meaning	Reference
IF ... THEN ... ELSE	Chooses between two values	IF
BRANCH	A multi-way conditional: a list of `IF ... THEN` lines and an `OTHERWISE`	BRANCH
CONSIDER	Pattern matching: picks a branch by the shape of a value	CONSIDER
WHEN	One branch of a CONSIDER	CONSIDER
OTHERWISE	The branch for every remaining case, in CONSIDER and BRANCH	CONSIDER
EXACTLY	In a pattern, matches a given value; in a regulative rule, matches an action exactly	CONSIDER

Operators

Operator	Meaning	Reference
AND, `&&`, `...`	Both are true	AND, OR, NOT, IMPLIES
OR, `\|\|`, `..`	At least one is true	AND, OR, NOT, IMPLIES
NOT	Negation	AND, OR, NOT, IMPLIES
IMPLIES, `=>`	If the first is true, so is the second	AND, OR, NOT, IMPLIES
UNLESS	`a UNLESS b` is `a AND NOT b`, binding more loosely than OR	UNLESS
PLUS, `+`	Addition; also adds days to a date	Arithmetic
MINUS, `-`	Subtraction	Arithmetic
TIMES, `*`	Multiplication	Arithmetic
DIVIDED BY, `/`	Division	Arithmetic
MODULO	Remainder of a division of whole numbers	Arithmetic
`%`	Percent after a number: `5%` is 0.05	Arithmetic
EQUALS, `=`	Equality	Comparisons
GREATER THAN, ABOVE, `>`	Greater than	Comparisons
LESS THAN, BELOW, `<`	Less than	Comparisons
AT LEAST, `>=`	Greater than or equal	Comparisons
AT MOST, `<=`	Less than or equal	Comparisons
FOLLOWED BY	Puts an item in front of a list	Operators
CONCAT	Joins strings: `CONCAT "a", "b"`	Built-in functions
`'s`	Reads a field: `person's age`	Syntax and directives

Regulative rules

Keyword	Meaning	Reference
PARTY	Who the rule applies to	PARTY, MUST, MAY, SHANT
MUST	Obligation	PARTY, MUST, MAY, SHANT
MAY	Permission	PARTY, MUST, MAY, SHANT
SHANT / MUST NOT	Prohibition; the two are synonyms	PARTY, MUST, MAY, SHANT
DO	An action neither required nor forbidden; without HENCE and LEST it behaves like MUST	PARTY, MUST, MAY, SHANT
PROVIDED	A condition the action must meet	Deadlines and consequences
WITHIN	The deadline, counted from when the rule starts	Deadlines and consequences
HENCE	What follows when the rule is complied with	Deadlines and consequences
LEST	What follows when it is not	Deadlines and consequences
FULFILLED	The end state: nothing more is owed	Deadlines and consequences
BREACH	The end state: a rule was broken; `BREACH BY party BECAUSE reason`	Deadlines and consequences
BY	Names the party in `BREACH BY`	Deadlines and consequences
RAND	Both rules apply at once	Deadlines and consequences
ROR	Either rule may be complied with	Deadlines and consequences
BECAUSE	The reason given for a breach	BECAUSE
DOES	In a trace event: `PARTY Seller DOES deliver AT 3`	EVENT
AT	The time of an event, or the start time of a `#TRACE`	EVENT

Files and modules

Keyword	Meaning	Reference
IMPORT	Uses the definitions of another file or a library	Standard libraries
TIMEZONE IS	Sets the document's time zone, an IANA name	timezone
`§`	Starts a section of the document; `§§` a subsection	Syntax and directives

Directives

Directive	Meaning	Reference
`#EVAL`	Evaluates an expression and shows the result	Syntax and directives
`#EVALTRACE`	Evaluates and shows each step	Syntax and directives
`#CHECK`	Shows the type of an expression without evaluating it	Syntax and directives
`#ASSERT`	Reports an error unless the expression is TRUE	Syntax and directives
`#TRACE`	Runs a regulative rule against events: `#TRACE rule AT 0 WITH ...`; `STARTING AT` is the same as `AT`	Syntax and directives

Annotations

Annotation	Meaning	Reference
`@desc`	A description of a definition, shown in tools and APIs	Syntax and directives
`@nlg`, `[...]`	Wording used when a rule is put into natural language	Syntax and directives
`@nlg:he`	A wording in a named language; a rule can carry one per language	Syntax and directives
`@lang he`	The language an untagged `@nlg` in the module is written in	Syntax and directives
`@ref`, `<<...>>`	A reference to the legal source	Syntax and directives
`@ref-src`, `@ref-map`	Where references are looked up	Syntax and directives
`@export`	Publishes a function as an API endpoint when the file is deployed	Syntax and directives
`@export default`	The function a deployment calls when no function is named	Syntax and directives

Symbols

Symbol	Meaning	Reference
`--`, `//`	A comment to the end of the line	Syntax and directives
`{- -}`, `/* */`	A comment over several lines	Syntax and directives
` `	Backticks around a name with spaces: `the applicant`	Syntax and directives
`"..."`	A STRING	Syntax and directives
`^`	Ditto: repeats the word above	Syntax and directives
`( )`	Groups an expression	Syntax and directives
`,`	Separates list items and arguments after OF	Syntax and directives
`_`	In a pattern, matches anything	CONSIDER
`_` between digits	Groups digits: `100_000` is 100000	Syntax and directives

Terms

Term	Meaning	Reference
Regulative rule	A rule about behaviour: who MUST, MAY or SHANT do what, by when, and what follows	Regulative rules
Constitutive rule	A rule that defines, classifies or calculates, written with DECIDE or MEANS	Functions
Deontic modality	Obligation (MUST), permission (MAY) or prohibition (SHANT/MUST NOT)	PARTY, MUST, MAY, SHANT
Defeasibility	A general rule giving way to an exception ("unless", "notwithstanding"), written with UNLESS or branches	UNLESS
Mixfix	A name with inputs between its words, such as borrower `pays` lender, so a call reads like a sentence	Functions
Isomorphism	Code that follows the structure of the legal text, clause for clause	Concepts
Residual obligation	What is still owed after some events: the DEONTIC value a `#TRACE` gives	DEONTIC
Reparation	A further obligation that follows a breach, written in a LEST	Deadlines and consequences
Clauses	A rule written as one line per case, each with values to match in place of its inputs; the first match applies	DECIDE
Exhaustiveness	Whether the branches of a CONSIDER, or the clauses of a rule, cover every case; L4 warns when they do not	CONSIDER