§

L4 Language Glossary

Complete reference index of all L4 language features. Links point to the consolidated reference pages which contain detailed documentation.

Keywords

Keywords are reserved words that form the structure of L4 programs.

Function Keywords

Keyword Purpose Reference
AKA Provides alternate names (aliases) AKA
DECIDE Defines a decision function DECIDE
FUNCTION Declares a function type TYPE-KEYWORDS
GIVEN Introduces function parameters GIVEN
GIVETH / GIVES Specifies function return type GIVETH
IN Used with LET for scoped bindings LET
LET Introduces a local binding LET
MEANS Defines the body of a function or decision MEANS
WHERE Introduces local declarations WHERE
YIELD Creates anonymous functions (lambdas) YIELD

Control Flow Keywords

Keyword Purpose Reference
BRANCH Alternative pattern matching keyword CONTROL-FLOW
CONSIDER Pattern matching on values CONSIDER
ELSE Alternative branch of IF CONTROL-FLOW
IF Conditional expression IF
THEN Consequent branch of IF CONTROL-FLOW
OTHERWISE Default case in CONSIDER CONTROL-FLOW
WHEN Introduces a pattern match case CONSIDER

Logical Keywords

Keyword Purpose Reference
AND / ... Logical conjunction AND
IMPLIES Logical implication IMPLIES
NOT Logical negation NOT
OR / .. Logical disjunction OR
UNLESS Exception clause (AND NOT) UNLESS

Comparison Keywords

Keyword Purpose Reference
ABOVE Synonym for GREATER THAN COMPARISONS
BELOW Synonym for LESS THAN COMPARISONS
EQUALS Equality test COMPARISONS
GREATER Greater than comparison COMPARISONS
LESS Less than comparison COMPARISONS
THAN Comparison conjunction word COMPARISONS
LEAST Used in "AT LEAST" (≥) COMPARISONS
MOST Used in "AT MOST" (≤) COMPARISONS

Type Keywords

Keyword Purpose Reference
A / AN Type articles ARTICLES
ASSUME Declares a variable of assumed type ASSUME
DECLARE Defines a type DECLARE
IS Type assertion or definition TYPE-KEYWORDS
HAS Record field declaration TYPE-KEYWORDS
LIST List type or list literal TYPE-KEYWORDS
ONE OF Used for enum types TYPE-KEYWORDS
OF Type application or constructor pattern TYPE-KEYWORDS
TYPE The kind of types TYPE-KEYWORDS
WITH Record construction with named fields TYPE-KEYWORDS
FOR ALL Universal quantifier for polymorphism FOR ALL

Regulative Keywords

For expressing legal obligations, permissions, and prohibitions.

Keyword Purpose Reference
PARTY Declares a legal party PARTY
MUST Obligation (deontic necessity) MUST
MAY Permission (deontic possibility) MAY
SHANT Prohibition SHANT
DO Optionality (deontic possibility) REGULATIVE
DOES Action verb in directive REGUALTIVE
EXACTLY Exact match/precision modifier REGULATIVE
WITHIN Temporal deadline REGULATIVE
HENCE Consequence (then) REGULATIVE
LEST Negative consequence (else) REGULATIVE
BREACH Violation of obligation REGULATIVE
BECAUSE Justification or reason for breach BECAUSE
PROVIDED Condition or proviso REGULATIVE
AT Temporal specification REGULATIVE

Arithmetic Keywords

Keyword Purpose Reference
PLUS Addition ARITHMETIC
MINUS Subtraction ARITHMETIC
TIMES Multiplication ARITHMETIC
DIVIDED Division (use with BY) ARITHMETIC
BY Division conjunction word ARITHMETIC
MODULO Modulus (remainder) ARITHMETIC

Other Keywords

Keyword Purpose Reference
IMPORT Imports definitions from another file IMPORT

Types

L4's type system includes primitive types, algebraic types, and polymorphic types.

For complete documentation, see Types Reference.

Primitive Types

Type Description
NUMBER Numeric values (integers and rationals)
STRING Text strings
BOOLEAN Truth values (TRUE, FALSE)
DATE Calendar dates

Polymorphic Types

Type Description
LIST Ordered collection of elements
MAYBE Optional values (JUST x or NOTHING)
EITHER Choice between two values (LEFT or RIGHT)

Special Types

Type Description
TYPE The kind of types
FUNCTION Function types

Operators

For complete documentation, see Operators Reference.

Symbolic Operators

Operator Textual Form Description
* TIMES Multiplication
+ PLUS Addition
- MINUS Subtraction
/ DIVIDED BY Division
>= AT LEAST Greater than or equal
<= AT MOST Less than or equal
> GREATER THAN / ABOVE Greater than
< LESS THAN / BELOW Less than
= EQUALS Equality
&& AND Logical conjunction
|| OR Logical disjunction
=> IMPLIES Logical implication

List Operators

Operator Description
FOLLOWED BY List cons (prepend element)
EMPTY Empty list

String Operators

Operator Description
CONCAT String concatenation
APPEND String concatenation (infix)

Temporal Operators

Operator Description
AT Point in time
WITHIN Time duration constraint

Syntax Patterns

Special syntax features and patterns in L4.

For complete documentation, see Syntax Reference.

Feature Description
Layout Rules Indentation-based grouping
Comments -- line comments and {- -} block comments
Identifiers Backtick-quoted identifiers
Annotations @desc, @nlg, @ref, @export
Directives #EVAL, #TRACE, #CHECK, #ASSERT
Ditto ^ copy from previous line
Asyndetic ... (AND) and .. (OR) implicit operators
Genitive 's for record field access
Section Markers § for document sections

Symbols

Symbol Name Purpose
() Parentheses Grouping, tuples
{} Braces Block comments
[] Square brackets NLG inline annotations
<<>> Double angles Reference annotations
§ Section symbol Document sections
^ Caret Ditto (copy above)
, Comma Separator
; Semicolon Statement separator
. Dot Decimal point, punctuation
... Ellipsis Asyndetic AND
.. Double dot Asyndetic OR
: Colon Type signature separator
% Percent Percentage, NLG delimiter
's Genitive Possession/field access

Literals

Literal Type Syntax Example
Integer Digits 42, -17
Rational Digits with decimal point 3.14, -0.5
String Double quotes "hello world"
Boolean TRUE or FALSE TRUE, FALSE
List LIST or FOLLOWED BY LIST 1, 2, 3

Core Libraries

Libraries shipped with L4.

For complete documentation, see Libraries Reference.

Library Purpose
prelude Standard functions (always imported)
daydate Date calculations and temporal logic
excel-date Excel date compatibility
math Mathematical functions
currency ISO 4217 currency handling
legal-persons Legal entity types
jurisdiction Jurisdiction definitions
llm LLM API integration

Built-in Functions

These are built into the compiler (not a library):

Type Coercion

Function Purpose
TOSTRING Convert to STRING
TONUMBER Convert to NUMBER
TODATE Convert to DATE
TRUNC Truncate number

See coercions documentation for details.

HTTP and JSON

Function Purpose
FETCH HTTP GET request
POST HTTP POST request
ENV Read environment variable
JSONENCODE Convert value to JSON string
JSONDECODE Parse JSON string to value

See HTTP and JSON documentation for details.

Directives

Compiler directives for testing and evaluation.

Directive Purpose
#EVAL Evaluate and print expression
#EVALTRACE Evaluate with execution trace
#TRACE Contract/state graph tracing
#CHECK Type check expression
#ASSERT Assert truth value

Annotations

Metadata annotations for documentation and generation.

Annotation Purpose
@desc Human-readable description
@nlg Natural language generation hint
@ref Cross-reference to legal source
@ref-src Source reference
@ref-map Reference mapping
@export Mark for export

Built-in Constants

Constant Type Description
TRUE BOOLEAN Boolean true value
FALSE BOOLEAN Boolean false value
NOTHING MAYBE a Absence of value
JUST a → MAYBE a Present value constructor
LEFT a → EITHER a b Left alternative
RIGHT b → EITHER a b Right alternative
EMPTY LIST a Empty list