A list of key-value pairs used as a simple lookup table, where
each entry pairs a key with a value.
C
Chain of Responsibility
A design pattern in which a request is passed along a sequence of
handlers, each of which either processes it or passes it on to the
next.
computer algebra system
A program that manipulates mathematical expressions symbolically
rather than numerically, such as Maple or Mathematica.
content-addressable
Storage in which data is identified by a hash of its content
rather than by a name or location.
context
A mapping from variable names to values that a template engine
uses when filling in placeholders.
currying
Transforming a function that takes multiple parameters into a
sequence of functions each taking a single parameter.
D
destructuring
Unpacking values from a composite type such as a tuple or
structure into individual bindings.
discard pattern
A binding that uses _ or a name starting with _ to intentionally
ignore a value. In a do block, let _ := expr silently discards
the result and suppresses the unused-variable compiler warning.
discrete event simulation
A method of modeling a system where time advances in jumps from
one event to the next rather than in fixed steps.
Domain Specific Language (DSL)
A programming language specialized to a particular application
domain, such as a build system or test framework.
E
effectful
Describing a computation that performs side effects such as
printing, reading input, or modifying state.
encapsulation
Hiding the internal implementation of a component behind a stable
interface, so that the implementation can change without affecting
code that uses it.
enumeration
A type defined by listing all of its possible values as named
constructors, created with inductive in Lean.
G
glob
A pattern-matching syntax for file names in which * matches any
sequence of characters and ? matches exactly one character.
I
inductive type
A type defined by listing its constructors; values are built from
those constructors and taken apart with pattern matching.
inverse-CDF method
A technique for generating random samples from a probability
distribution by inverting its cumulative distribution function; if
U is uniform on (0,1) then F⁻¹(U) follows the target distribution.
L
Lake
Lean's build tool and package manager, analogous to cargo in
Rust.
lakefile
A configuration file (typically lakefile.lean) that declares a
package's dependencies and build rules for Lake.
language server
A program that implements the Language Server Protocol to provide
editor features such as error highlighting, autocompletion, and
go-to-definition.
lemma
A named intermediate statement that has been proved, used to
simplify larger proofs by breaking them into smaller steps.
linear congruential generator
A simple pseudorandom number generator defined by the recurrence
seed' = (A × seed + C) mod M. The same seed always produces the
same sequence.
log-structured
A storage design where all writes are appended to a sequential log
rather than updating records in place; the current value of a key
is found by scanning the log for the most recent entry.
M
monad
A design pattern that sequences computations while threading extra
information such as I/O state through each step.
O
Omega test
A decision procedure for integer Presburger arithmetic used by
Lean's omega tactic to solve linear arithmetic goals
automatically.
P
partial
A keyword that tells Lean to skip termination checking for a
function. Used when a function is known to terminate but Lean's
automatic checker cannot prove it.
point-free style
A way of defining functions by composing other functions without
naming their parameters, using ∘ or |>. The "point" refers to
the argument value itself.
prelude
A standard library of basic types and functions automatically
available in every Lean file without an explicit import.
product type
A type that combines multiple values into a single compound value;
tuples and structures are product types.
proof term
A value whose type is a proposition; produced by tactics such as
rfl and omega.
proposition
A claim expressed as a type in Lean's type system; has type
Prop.
pure
Describing a function whose output depends only on its input
arguments and that has no observable side effects.
R
random number generator
An algorithm that produces a sequence of numbers that approximates
true randomness, driven by an initial seed value.
Read-Eval-Print Loop (REPL)
An interactive prompt where expressions are read, evaluated, and
their results printed immediately.
recursive data type
A data type that can contain instances of itself, such as a tree
whose nodes may themselves be trees.
recursive type
A type whose definition refers to itself, enabling structures of
unbounded depth such as lists and trees.
ring
An algebraic structure with addition and multiplication satisfying
rules such as commutativity, associativity, and distributivity;
integers, natural numbers, and polynomials are all rings.
S
saturating subtraction
Subtraction that stops at zero rather than producing a negative
result, so 3 - 5 = 0 instead of -2. Used by Lean's Nat
type.
sum type
A type whose value is exactly one of several distinct variants,
defined with inductive in Lean.
syntactic sugar
Syntax that makes code easier to read or write without adding new
capabilities to the language.
T
tactic
A command that constructs a proof automatically, such as rfl,
omega, or simp.
tagged union
Another name for a sum type; a value that is one of several
variants with a runtime tag indicating which variant is held.
template engine
A program that combines a template containing placeholders with a
context of values to produce output such as an HTML page.
termination
The property of a recursive function that it always reaches a base
case and halts rather than looping forever.
termination checking
Lean's automatic verification that every recursive function
eventually stops. Functions that cannot be proved terminating
must be marked partial.
tombstone
A marker record in a log-structured store indicating that a key
has been deleted, rather than removing the original entry.
type alias
An alternative name for an existing type, created to improve
readability without defining a new type.
type class
An interface that defines operations a type must support, such as
BEq for equality or Repr for display. Instances are generated
automatically with deriving or written by hand.
type parameter
A placeholder in a generic definition that is replaced with a
concrete type when the definition is used, such as α in List α.
W
workspace
A collection of related Lean packages managed together by Lake in
a shared build environment.