General documentation

index

foundational types

tactics

Library

Aesop (file)

Builder

Apply

Basic

Cases

Constructors

Default

Forward

NormSimp

Tactic

Unfold

BuiltinRules (file)

ApplyHyps

Assumption

DestructProducts

Ext

Intros

Rfl

Split

Subst

Forward

Match (file)

Types

State (file)

ApplyGoalDiff

Initial

UpdateGoal

LevelIndex

PremiseIndex

RuleInfo

SlotIndex

Substitution

Frontend (file)

Extension (file)

Init

Attribute

Basic

Command

RuleExpr

Saturate

Tactic

Index (file)

Basic

DiscrTreeConfig

Forward

RulePattern

Options

Internal

Public

Rule (file)

Basic

Forward

Name

RulePattern (file)

Cache

RuleSet (file)

Filter

Member

Name

RuleTac (file)

Forward (file)

Basic

Apply

Basic

Cases

Descr

ElabRuleTerm

GoalDiff

Preprocess

RuleTerm

Tactic

Script

Check

CtorNames

GoalWithMVars

Main

OptimizeSyntax

SScript

ScriptM

SpecificTactics

Step

StructureDynamic

StructureStatic

Tactic

TacticState

UScript

UScriptToSScript

Util

Search

Expansion (file)

Basic

Norm

Simp

Queue (file)

Class

ExpandSafePrefix

Main

RuleSelection

SearchM

Stats

Basic

Extension

File

Report

Tree

Data (file)

ForwardRuleMatches

AddRapp

Check

ExtractProof

ExtractScript

Free

RunMetaM

State

Stats

Tracing

Traversal

TreeM

UnsafeQueue

Util

Tactic (file)

Ext

Unfold

Basic

EqualUpToIds

OrderedHashSet

Unfold

UnionFind

UnorderedArraySet

BaseM

Check

Constants

EMap

ElabM

Exception

Main

Nanos

Percent

Saturate

Tracing

Batteries

Classes

Order

RatCast

CodeAction (file)

Attr

Basic

Deprecated

Match

Misc

Control

ForInStep

Basic

Lemmas

Nondet

Basic

AlternativeMonad

LawfulMonadState

Lemmas

OptionT

Data

Array

Basic

Match

Merge

BinomialHeap

Basic

BitVec

Basic

Lemmas

Fin

Basic

Lemmas

OfBits

List

Basic

Count

Lemmas

Pairwise

Perm

MLList

Basic

Nat

Bitwise (file)

Lemmas

Basic

Lemmas

String

Basic

Matcher

Except

Int

UInt

Lean

Meta

Basic

DiscrTree

Expr

Inaccessible

InstantiateMVars

SavedState

UnusedNames

AttributeExtra

Except

Expr

HashMap

HashSet

MonadBacktrack

NameMapAttribute

PersistentHashMap

PersistentHashSet

Position

Syntax

TagAttribute

Linter (file)

UnnecessarySeqFocus

UnreachableTactic

Tactic

Lint (file)

Basic

Frontend

Misc

Simp

TypeClass

Alias

Basic

Case

Congr

Exact

GeneralizeProofs

HelpCmd

Init

OpenPrivate

PermuteGoals

SeqFocus

Trans

Unreachable

Util

Cache

ExtendedBinder

LibraryNote

ProofWanted

Logic

Complexitylib (file)

Algebraic (file)

Analysis (file)

Degree

Depth

Frontier

Polarity

PossibleValues

Support

Applications (file)

Hessian

Waring

Basis

AC0 (file)

Normalization

Restriction

Aggregate (file)

Examples

AndOr (file)

Preimage

Arithmetic (file)

Expression

Power

Binary (file)

Formula

DeMorgan (file)

Arithmetic

CSLib

CircuitAnalysis

CircuitRestriction

Completeness

Complexity

Dependency

Expression

Influence

Mask

NativeCost

Operations

Origin

PairIndicator

PointUpdate

ReadOnce

Residual

Restriction

RestrictionAnalysis

ShannonLupanov

Threshold

TightCircuit

Wiring

FiniteSupport

JoinMeet

SumOfTerms

BooleanCube (file)

ModThree (file)

Cube (file)

Defs

Internal

Blocks

Defs

Internal

Kernel

Neighbors

CircuitFamily (file)

Growth

Combinatorics

FiniteCover

Sunflower

Complexity (file)

Relative

RelativeApproximation

RelativeCounting

RelativeSupport

RelativeTransport

ConditionalComplexity (file)

Boolean

Counterexample

Counting

Linear

Restriction

Counting (file)

Syntax

LinearAlgebra

MatrixRank (file)

Internal

NonsingularMinor (file)

Internal

Tensor

DeletionGame (file)

Defs

Internal

Diagonal (file)

Paired (file)

Internal

Defs

Internal

Dissociated (file)

Defs

Internal

Explicit (file)

Defs

Internal

Internal

BorderRank

Koszul (file)

Defs

Internal

Periodic (file)

Internal

Substitution (file)

Defs

Internal

BorderRank

Defs

Rank

LowerBound (file)

AC0

Switching (file)

Canonical

CanonicalEncoding

CombinedAdvice

CombinedCanonical

CombinedCanonicalEncoding

CombinedCanonicalPacking

CombinedCanonicalTrace

Encoding

Family

BottomFamily

BottomGate

CanonicalDecisionTree

DecisionTree

DecisionTreeTrace

Duality

Layer

LayerExistence

LayerExistenceBounds

LayerFormula

LayerIteration

LayerIterationBounds

LayerSchedule

LayerSwitching

LayerSwitchingBounds

LiteralGate

NormalForm

Parity

ParityCircuit

ParityDepthReduction

ParityLowerBound

ParityNormalForm

ParityParameters

ParityRoot

ParityScale

ParitySeparation

ParitySizeArithmetic

ParitySurvivors

ParityTopGate

RandomRestriction

RestrictionAveraging

TreeNormalForm

Counting (file)

AlmostAll

Arity

Basic

Coarse

Depth

FinalTerm

Normalization

Shannon

Sharp

Cutwidth (file)

Aggregate (file)

Capacity (file)

Circuit (file)

Count

Defs

Internal

RealCount

Asymptotics

Hardness

LowerBound

Polarity

Circuit (file)

Count

Defs

Graph

Internal

Mixing

Observation

Compressed

Basic

Compilation

Components

Defs

Generated

Hardness

LowerBound

Modular

ModularHardness

Observation

Geometry (file)

Affine (file)

Shared (file)

Matching (file)

Defs

Internal

Count

Preprocess

Relative

Basic

Coset

Count

Defs

Direction

Lines

Pairing

Entropy (file)

Finite (file)

Bias

Counting

Uniform

Graph (file)

Internal

Assembly

Bound

Constants

Insert

Weights

Defs

Support

Local (file)

Cases (file)

Defs

Internal

Coordinates

Defs

Empirical

Numbers

Pair (file)

Defs

Internal

Averaging

Collisions

Fibres

OneWay

Weighted

Fiber

Conditional

Asymptotics

Counting

Entropy

Hardness

Internal

Inversion

LowerBound

Message

Multioutput

OneWay

Parameters

Retention

Weights

Entropy (file)

Internal

Asymptotics

Circuit

Counting

Defs

Hardness

Internal

Inversion

LowerBound

Message

Multioutput

OneWay

Parameters

FieldMul (file)

Defs

Internal

Gold (file)

Encoding

Field

Parameters

Properties

Inversion (file)

Collisions

Components

Encoding

Features

Field

Parameters

Properties

Joint

Conjunction

Basic

Bias

Defs

Family

Refined

SharedAveraging (file)

Weighted

SharedMessage (file)

Basic

Defs

Internal

Asymptotics

Averaging

Hardness

LowerBound

Message

OneWay

Parameters

Message (file)

Bias

Defs

Internal

Multioutput (file)

Features (file)

Internal

Rank (file)

Defs

Internal

RestrictionRank (file)

Defs

Internal

ConjunctionEntropy

Counting

Entropy

LowerBound

Outputs

Shared

Asymptotics

Hardness

LowerBound

Parameters

Asymptotics

Defs

Hardness

LowerBound

Model

Parameters

Internal

Network

Wiring (file)

Defs

Graph

Reindex

Semantics

Asymptotics

Compilation

Components

Family

Hardness

LowerBound

Network

NetworkDefs

OneWay

Ordering

Rectangle

Restriction

Concentrator (file)

Acyclic (file)

Internal

Defs

Internal

Extractor (file)

Condenser

Encoding (file)

Correctness (file)

Internal (file)

Basic

Frobenius

Horner

Packing

Source

Linear (file)

Internal

Defs

Explicit (file)

Block (file)

Program (file)

Correctness (file)

Internal

Defs

Internal

Lossless (file)

Internal

Pair (file)

Splitting (file)

Internal

Unary (file)

Internal

Defs

Internal

Weighted (file)

Internal

Defs

Internal

Lossless (file)

Internal

Serialization (file)

Defs

Internal

Defs

Internal

Expansion (file)

Primitive (file)

Internal

Quotient (file)

Internal

Defs

Internal

Interpolation (file)

Internal

Lossless (file)

Mixture (file)

Defs

Internal

Polynomial (file)

Internal

Defs

Internal

Modulus

Binary (file)

Codec (file)

Defs

Internal

Encoding (file)

Defs

Internal

Extension (file)

Defs

Internal

Internal (file)

Basic

Irreducible

Defs

Binomial (file)

Extension (file)

Internal

Defs

Internal

Monomials (file)

Defs

Internal

Parameters

Explicit (file)

Unary (file)

Internal

Defs

Internal

Sparse (file)

Defs

Internal

Polynomial (file)

Defs

Internal

Substitution (file)

Defs

Internal

Conditioning (file)

Internal

CorrelationBreaker

Advice (file)

Extraction (file)

Alternating (file)

Defs

Internal

Internal (file)

Initial

Parameters (file)

Internal

Perturbed (file)

Internal

Program (file)

Defs

Internal

Defs

Internal (file)

Invariant

Bounds (file)

Basic

Closed

Defs

Reserves

Iteration (file)

Basic

Step (file)

Build

Comparison

Defs

Final

Initial

Parameters (file)

Defs

Internal

Program (file)

Internal (file)

Run

Defs

Truncation (file)

Defs

Internal

Defs

Affine

Iteration (file)

Extraction (file)

Internal

Actual

Induction

Parameters

Rows

Defs

Initial (file)

Internal

Basic

Envelope

Execution

Defs

Internal

Basic

Envelope

Execution

Parameters (file)

Internal

Basic

Error

Mass

Polynomial

Reserves

Round

Defs

Program (file)

Defs

Internal

Defs

PhaseOne

Extraction (file)

Bounds (file)

Internal

Parameters (file)

Internal

Defs

Internal

Final (file)

Internal (file)

Mask

Defs

Initial (file)

Internal

Parameters (file)

Unary (file)

Internal

Defs

Internal

Program (file)

Parameters (file)

Defs

Internal

Defs

Internal

Second (file)

Defs

Internal

Subset (file)

Internal (file)

Projection

Defs

Transcript (file)

Internal

Basic

Envelope

Defs

Program (file)

Defs

Internal

Round (file)

Envelope (file)

Defs

Extraction (file)

Bounds (file)

Internal

Defs

Internal

Final (file)

Internal (file)

Basic

Extraction

Mask

Projection

Defs

Internal

Envelope

Bounds

Totals

Basic

Factorization

Invariant (file)

Defs

Internal

Middle (file)

Internal (file)

Left

Mask

Defs

Parameters (file)

Internal

Program (file)

Defs

Internal

Recovery (file)

Internal

Seed (file)

Defs

Internal

Subset (file)

Internal

Transcript

Defs

Defs

Defs

FlipFlop

LookAhead (file)

Defs

Internal

Opposite

False (file)

Internal

True (file)

Internal (file)

Repair

UniformState (file)

Internal (file)

Repair

Defs

Preservation

Half (file)

Internal (file)

Capped

Defs

Step (file)

Internal (file)

First

Weak (file)

Internal (file)

Basic

Identity

Program (file)

Defs

Internal

Transcript (file)

Internal

Basic

Envelope

Output (file)

Internal

Basic

Envelope

Defs

Defs

UniformState (file)

Internal

Defs

FourthMoment (file)

Internal

Hashing (file)

Binary (file)

Defs

Internal

Field (file)

Defs

Internal

Internal (file)

Counting

SecondMoment

Defs

Majority (file)

Probability (file)

Internal

Defs

Internal

Moments (file)

Tails (file)

Internal

Defs

Internal

Padding (file)

Asymptotics (file)

Internal

Defs

Internal

Sampler (file)

Amplification (file)

Defs

Internal

Reindex (file)

Internal

Defs

Internal

SourceReduction (file)

BadSeeds (file)

Defs

Internal

Construction (file)

Asymptotics (file)

Internal (file)

Bounds

Growth

Hardness (file)

Internal

Internal (file)

Basic

Sampler

Program (file)

Internal

Computation

Correctness

Defs

Uniform (file)

Internal (file)

Basic

Parameters

Defs

Defs

Encoding (file)

Defs

Internal

Leakage (file)

Average (file)

Internal (file)

Conditioning

BadSeeds (file)

Internal

Linear (file)

Internal

Selected

Parameters (file)

Defs

Internal

Parity (file)

Internal

Defs

Parameters (file)

Defs

Internal

Reduction (file)

Defs

Internal

Sampler (file)

Internal (file)

Basic

Program (file)

Defs

Internal

Defs

Selection (file)

Internal

Tests (file)

Internal (file)

Estimate

Slots

Defs

Internal

Strong (file)

Block (file)

Condenser (file)

Extraction (file)

Internal

Internal (file)

Basic

Hybrid

Repair (file)

Internal (file)

Replacement

Transport

Conditioning (file)

Internal (file)

Prefix

Prepend

Internal (file)

Two

Level (file)

Extraction (file)

Internal

Defs

Internal

Recursion (file)

Extraction (file)

Defs

Internal

Initial (file)

Internal

Internal (file)

Bounds

Linearity (file)

Internal

NearHalving (file)

Boolean (file)

Defs

Internal

Codec (file)

Defs

Internal

Gamma (file)

Padded (file)

Defs

Internal

Program (file)

Family (file)

Internal

Defs

Internal

Defs

Internal

Parameters (file)

Asymptotics (file)

Internal

Explicit (file)

Defs

Internal

Unary (file)

Internal

Defs

Internal

Program (file)

Correctness (file)

Internal

Defs

Internal

Run (file)

Correctness (file)

Internal

Defs

Internal

Defs

Internal

Parameters (file)

Explicit (file)

Internal

Defs

Internal

Scheduled (file)

Affine (file)

Internal

Asymptotics (file)

Defs

Internal

Boolean (file)

Defs

Internal

BoundedDepth (file)

Internal

Codec (file)

Defs

Internal

Internal (file)

Components

Linearity (file)

Internal

Matched (file)

Affine (file)

Internal

Growing (file)

Program (file)

Defs

Internal

Internal

Program (file)

Defs

Internal

Defs

Internal

Program (file)

Correctness (file)

Internal

Family (file)

Defs

Internal

Defs

Internal

Run (file)

Correctness (file)

Internal

Defs

Internal

Seeds (file)

Internal

State (file)

Parameters (file)

Defs

Internal

Defs

Internal

Defs

Defs

Splitting (file)

Iterated (file)

Family (file)

Internal

Internal (file)

Hybrid

Prepend

Transport

Tuples

Defs

Defs

Internal

Defs

Composition (file)

Internal (file)

Tests

FlatMixture (file)

Internal (file)

Birkhoff

OneShot (file)

Block (file)

Program (file)

Defs

Internal

Correctness (file)

Internal

Extraction (file)

Internal (file)

Composition

Hashing

Parameters (file)

Defs

Internal

Weighted (file)

Internal

Defs

Internal

Weighted (file)

Affine (file)

Defs

Internal

Alternating (file)

Copies (file)

Defs

Internal

Defs

Internal

Condenser (file)

Identity (file)

Internal

Internal (file)

Basic

Transport (file)

Internal

Defs

Conditional (file)

Transport (file)

Internal

Defs

Internal

Coupling (file)

Conditional (file)

Internal

Factored (file)

Internal (file)

Basic

Transfer

Defs

Internal

Basic

Lifting

Maximal

Projection

Equiv (file)

Internal

Expectation (file)

Internal

Leakage (file)

Internal

LookAhead (file)

FixedTampering (file)

Internal (file)

Basic

Second (file)

Internal (file)

Basic

Defs

Defs

Internal (file)

Basic

Refresh (file)

Internal

Basic

Envelope

Factorization

First

Second

Defs

UniformRefresh (file)

Internal (file)

Basic

Extract

Defs

UniformState (file)

Internal (file)

Basic

Defs

Merging (file)

Independence (file)

Defs

Internal

Internal (file)

Basic

Distance

Envelope

Smooth (file)

Independence (file)

Defs

Internal

Internal (file)

Basic

Repair

Seed

Uniform

Defs

Defs

Mixture (file)

Internal

Perturbation (file)

Internal

Probability (file)

Internal

Projection (file)

Internal

SeedPadding (file)

Internal

SeedStep (file)

Defs

Internal

Transcript (file)

Distance (file)

Internal

Envelope (file)

Internal

Defs

Internal

Defs

Internal

Defs

Internal

Defs

Gaussian (file)

Band (file)

Internal

Assembly

Limit

Order (file)

Internal

Defs

Edge (file)

Decay (file)

Internal

Exact (file)

Internal

Defs

Internal

Frontier (file)

Arccos (file)

Internal

Internal

Assembly

Expectation

Limit

Vector

Order (file)

Defs

Internal

Star (file)

Defs

Internal

Defs

Kernel (file)

Defs

Internal

Layout (file)

Internal

Assembly

Expectation

Grid

Limit

Local

Defs

SecondMoment (file)

Internal

Halver (file)

Defs

Internal

Hyperconcentrator (file)

Defs

Internal

MultiOutput

DFT (file)

Defs

Internal

FieldMul (file)

Defs

Internal

Linear (file)

Defs

Rank

MatMul (file)

Arithmetic (file)

Accounting

Defs

Internal

Rank

Internal

Bound

Charge

Component

Coordinates

Kernel

Tripartite (file)

Defs

Internal

Defs

Ordering (file)

Internal (file)

Graph

PolyMul (file)

Defs

Internal

Polynomial (file)

Arithmetic (file)

Internal

Cauchy

Defs

Internal

Linearization

Quadratic (file)

Defs

Internal

Polynomial

Rank (file)

Internal

Restrict (file)

Defs

Internal

Taylor (file)

Defs

Internal

TotallyRegular (file)

Internal

CauchyCharZero

Defs

PathDecomposition (file)

Bisection (file)

Amplification (file)

Internal

BoundaryLift (file)

Defs

Internal

BoundaryNormalization (file)

Internal

EdgeSwitch (file)

Defs

Internal

Helpful (file)

Internal

Improvement (file)

Defs

Internal

Internal (file)

Assembly

LocalConfigurations (file)

Internal

NeighborNormalization (file)

Internal (file)

Potential

State

Rebalancing (file)

Internal

RedBlack (file)

BridgeQuotient (file)

Internal (file)

Regions

Defs

Clusters (file)

Density

Internal

Internal (file)

Incidence

Partition

ConnectedPartition (file)

Internal (file)

Assembly

Defs

Regions

CycleRemoval (file)

Internal (file)

Core

Rank

PathSuppression (file)

Internal (file)

Counting

Regions (file)

Defs

Internal

Defs

PathSystem (file)

Internal (file)

Attachments

Core

Isolation

SpanningPath

Thin

Marks (file)

Internal (file)

Endpoints

Defs

Defs

Restoration (file)

Family (file)

Core (file)

Internal (file)

Structure

Weighted

Marks (file)

Defs

Internal

Defs

Internal

Internal

Defs

Internal

Reduction (file)

Internal

Suppression (file)

Defs

Internal

WeightedTree (file)

Internal

Defs

Boundary (file)

Internal

Components (file)

Internal

CutBoundary (file)

Defs

Internal

Endpoint (file)

Internal

Glue (file)

Internal

Operations (file)

Defs

Internal

Padding (file)

Internal

Tree (file)

Internal

TreeComponent (file)

Internal

SingleCut (file)

Defs

Internal

Superconcentrator (file)

Internal

Bound

Cut

Lift

Split

Defs

Wiring (file)

Signals

Asymptotics

AverageCase

Balanced

Compression

Direction

Expansion

Forget

FourN

MedianOrdering

Multigraph

Network

Nondeterministic

Rectangle

FanIn (file)

Depth

Size

Fusion (file)

Arithmetic (file)

Interaction (file)

Hessian (file)

Pairing

PairingRelative

Pairwise

Relative

Linear (file)

Quotient

Polynomial (file)

Catalecticant (file)

Rectangular (file)

Profile (file)

Decomposition

Multiplication

Decomposition

Degree

Decomposition

Degree

Squarefree (file)

Mixing

Mixing

Nonlinear

Quotient

Rank (file)

Local

Occurrence

Multiple

MonotonePolynomial (file)

Exact

Layer

MultiplicativeShadow (file)

Pairwise

Polynomial

Progress (file)

Separated (file)

Clique (file)

Exact

NNRat

NaturalConstants

PositiveConstants

Total

Closure (file)

Weighted (file)

Addition

Exact

NNRat

Addition

PositiveConstants

Addition

Collision

Expansion

MonomialSubstitution

Polynomial

Unit

WeightedMonomialSubstitution

General

Atoms

BoundedFailure

Combined

Degree

ExactSupport

Expression

Power

Support

Conondeterministic (file)

Neq

Cyclic (file)

Closure

Compiler

Complete

JoinMeet

LowerJoinMeet

Neq

Graph

Canonical

Neq (file)

Preimage

SumOfTerms (file)

MatrixRank (file)

Cover (file)

Identity

Block

BlockSum

Support

Waring (file)

Rectangular (file)

Restriction

Binary (file)

Compilation

Translation

Binary

Restriction (file)

Binary (file)

Compilation

Translation (file)

Binary

Coverage

Rank

Rectangle

WeightedRank

Boolean

Comap

Contextual

Counting

CrownCollision

Framework

Pullback

Semifilter

Substitution

GateElimination (file)

DeMorganXor

Framework

Translation

Xor

Hierarchy (file)

Family

Finite

Polynomial

KarchmerWigderson (file)

Sharing (file)

Extended (file)

Defs

Internal

Circuit

UpperBound

Basic

Composition

Khrapchenko

MCSP (file)

Defs

Nechiporuk

NonVacuity

SubcubeRepetition

Symmetry

Monotone

Clique

Approximation

Asymptotic

Basic

Essential

Exponential

LowerBound

Negative

Plucking

Positive

MatrixProduct (file)

NegationLimited (file)

Internal

Internal

Partial

Nechiporuk (file)

Sharing (file)

Defs

Internal

Subfunctions

Threshold (file)

Internal

Activation

Capacity

Changes

Corollaries

Family

Program

Defs

Family

Approximation

MassProduction (file)

HighRate (file)

BooleanRecovery

Code

CodePacking

DigitMonomials

Independence

LineParity

Packing

PolynomialSupport

PrefixMetadata

Rate

Residue

ResourceLayout

Systematic

Nonuniform (file)

AdjacentDuplicates

AffineMenuPoints

BatchLookup

BatchLookupBound

BatchOr

BatchOrCircuit

BatchOrLayout

BatchRouting

BatchRoutingBound

BatchRoutingLayout

BinaryPhaseMenu

BlockParameters

BroadcastCircuit

BroadcastCorrectness

BroadcastRecords

BufferAdvance

BufferEndpoints

BufferInput

BufferIteration

BufferIterationCost

BufferLineIncidences

BufferModel

BufferModelAdvance

BufferOccupancy

BufferOrder

BufferPhaseState

BufferResourceEvaluation

BufferResourceWires

BufferStepCorrectness

BufferTransform

BufferedPhase

BufferedPhaseCost

CandidateSelection

CanonicalBroadcast

CodeQuantitative

CoefficientParameters

CollisionCut

CollisionTail

ConditionalCounting

ConstantTranslations

DuplicateFlags

EnumeratedClean

EventualParameters

FiniteBound

FlagSelection

FlaggedRows

GeometricPhaseCircuit

GeometricPhaseCorrectness

GeometricPhaseCost

GeometricPhaseLayout

GeometricPhaseOutput

GeometricSlopes

GroupClean

HalvingCounts

IncidenceEvaluation

KeyedSort

LeadingCost

LupanovRuntime

MarkDuplicates

MaskedOr

MaskedScatter

MaskedXor

Menu

MenuClean

MenuPointLayout

MenuSelection

OrderedPermutation

OverheadPolynomial

PaddedLinePoints

PaddedLineRecovery

PaddedPhaseMenu

PhaseMenu

PhaseOccupiedMembership

PhaseSelection

PointConflicts

PowerLayout

PreparedInputs

Propagation

RealParameters

RealTheorem

RecordArray

ResourceBank

ResourceGather

RestoreRequestOrder

RoutingSources

RuntimeComposition

ScheduledRecovery

SchedulerCircuit

SelectRows

SharpTheorem

SortedPropagation

TaggedBuffer

UniversalGeometricPhase

SortingSemantics (file)

Boolean

Defs

Internal

BaseConversion

BinaryEncoding

BinaryField

BlockInduction

BlockInductionFiniteStep

BlockInductionLedger

BlockInductionOverhead

BlockInductionParameters

BlockInductionStep

BlockInductionVolumeBound

CanonicalMetadataRouting

CanonicalPacking

CanonicalRouting

CanonicalScatter

CodeParameters

CompositionBound

DirectProduct

DynamicGatherDecoder

DynamicPipelineAssembly

EqualBlock

EqualBlockFiniteStep

EqualBlockLedger

EqualBlockOverhead

EqualBlockParameters

EqualBlockVolumeBound

EvaluationCode

FiniteMassProductionCircuit

FiniteParameters

FixedDivision

ForbiddenRanks

FreshDirection

GatherAssembly

GatherDecoder

GatherRouting

GroupedRecovery

GroupedScheduler

Growth

IncidenceRouting

InputSplit

LeastMissing

LineEnumeration

LowDegree

LupanovCircuit

LupanovParameters

LupanovPatternBank

LupanovSynthesis

LupanovTable

OverheadBound

PackedGroupedRecovery

PackedPipeline

Padding

PipelineAssembly

Projective

ProjectiveCircuit

ProjectiveRank

Recovery

ResourceEvaluation

ResourcePacking

Routing

RoutingAssembly

RoutingCorrectness

RoutingMetadata

RoutingPasses

RoutingRecords

RoutingWiring

RuntimePacking

RuntimePipeline

RuntimeRequestData

RuntimeScheduleAssembly

ScalarSynthesis

ScatterAssembly

ScatterResourceAssembly

ScheduledRecovery

ScheduledRoutingWiring

Scheduler

SchedulerIteration

SchedulerStage

ShannonCircuit

ShannonParameters

ShannonSynthesis

Sorting

SortingBy

SortingCorrectness

SortingNetwork

Statement

Uhlig

UhligAsymptoticBounds

UhligCircuit

UhligDecoder

UhligFiniteTheorem

UhligLayer

UhligLayerBound

UhligParameters

UhligRecursion

UhligRecursiveCircuit

UhligRoutingCircuit

UhligTheorem

Translation (file)

Block

Category

Contextual

Metric

Optimal

Circuit

Compaction

Core

Cost

Fin

Homomorphism

Interpretation

Iteration

Parallel

PartialAssignment

Program

Reduction

Restriction

Semantics

Signature

Simulation

Substitution

Support

Asymptotics (file)

PolyBound

PolynomialComposition

BooleanAnalysis (file)

Bernoulli (file)

Defs

Internal

CoordinateSampling (file)

Internal

Fibers (file)

Internal (file)

Resampling

Defs

FourierExpansion (file)

Defs

Internal

HarmonicMean (file)

Internal

Cube

Density

Inequality

Mean

Projection

Properties

Reindex

Defs

LightPatterns (file)

Defs

Internal

MirrorSets (file)

Internal

Completion

Guiding

Defs

PolynomialCorrelation (file)

Internal

Binomial

Blocks

Bridge

Counting

Filtration

FiniteBound

Interpolation

Multiplication

Reduction

Defs

PolynomialThreshold (file)

Internal

BinomialMoments

BlockCoupling

BlockVanishing

Bridge

Commutator

CoordinateDegree

CoordinateMultipliers

CubeOperators

EdgeRecovery

FiniteCoupling

GradingShift

HilbertSchmidt

Main

Model

Multilinearize

PolynomialDegree

ProjectionBlocks

ProjectionTrace

ScalarIncrements

SignParity

Statement

Walsh

WalshDimensions

WeightedGrading

Defs

Sensitivity (file)

Internal

Basic

Composition

ConstructedSeed

Construction

DecisionTree

FixedCoordinates

HammingBase

InitialPredicates

Iterates

Labeling

LabelingBounds

LabelingConstraints

LabelingEstimate

LabelingEvents

Or

ParameterBounds

PowerAmplification

ProfileArithmetic

QuantitativeProfiles

QuerySeparation

Recursive

RecursiveBlocks

RecursiveCandidates

RecursiveChildren

RecursiveDefinitions

RecursiveFailures

RecursiveFlips

RecursiveJointZero

RecursiveOne

RecursiveProfiles

RecursiveRepair

RecursiveSets

RecursiveZero

Reindex

ScalarBounds

SeedAmplification

Separation

SeparationArithmetic

Tournament

TournamentCounts

TournamentCyclic

Tower

TowerProfiles

Defs

ThresholdWeight

Circuits (file)

AC0 (file)

Compilation (file)

Defs

Internal

Iteration (file)

Defs

Internal

NormalForm (file)

Connectives

Defs

Internal

Normalization (file)

Cslib (file)

Defs

Internal

Defs

Internal

Parity (file)

Internal

Separation (file)

Internal (file)

Majority

Switching (file)

Collection (file)

Defs

Internal

Parity (file)

Internal

Defs

Internal

Defs

Restriction

AndOrMod

Defs

AndOrNot (file)

Defs

BarringtonCodeGenerator (file)

Defs

Internal

BarringtonCompiler (file)

Defs

Internal

BarringtonConverse (file)

Defs

Internal

BarringtonTyped (file)

Defs

Internal

Basis

Defs

BasisHom (file)

Defs

Internal

BinaryComparison (file)

Defs

Internal

BinaryMinimum (file)

Defs

Internal

BranchingProgramEncoding (file)

Defs

Internal

CircuitFormula (file)

Family (file)

Defs

Internal

Defs

Internal

Composition (file)

Defs

Internal

Correlation (file)

Internal

Asymptotics

Bipartite

Circuit

Classes

Counting

Lindsey

Rank

Rectangle

Defs

DecisionTree (file)

Block (file)

Defs

Internal

Finite (file)

Defs

Internal

NormalForm (file)

Defs

Internal

Path (file)

Defs

Internal

Restriction

Dependency (file)

Defs

Internal

DepthClasses (file)

Defs

Internal

DepthThree (file)

Internal

Basic

Explicit

LowerBound (file)

Balanced (file)

Defs

Internal

AlgebraBits

AlgebraFiniteFibers

AlgebraLanguage

AlgebraPolynomial

AlgebraQuotient

AsymptoticBounds

Balanced

Circuit

CircuitDeletion

CircuitDensity

CircuitLowerBound

CircuitNormalization

CircuitQuantitative

Core

CorrelationTransfer

Cslib

CylinderProbability

Entropy

EntropyBits

EntropyThreshold

FinalParameterBounds

FiniteProbability

FiniteProbabilityBounds

FormulaNormalization

HardSlice

HardSliceEventual

HardSliceExistence

HardSliceMoment

HardSliceParameters

HardSliceProbability

HardSliceSelection

Hash

HashAffine

HashBool

HashFibers

HashProbability

HashTriangular

InterpolationEvaluation

InterpolationQuotient

InterpolationSigns

IrreducibleEncoding

IrreduciblePolynomial

Language

LanguageBitArithmetic

LanguageBitConvolution

LanguageBitConvolutionUpdates

LanguageBitEvaluator

LanguageBitHashUpdates

LanguageBitHornerLoop

LanguageBitLoopInvariants

LanguageBitReductionLoop

LanguageBitWord

LanguageInputBlockLists

LanguageInputBlockWords

LanguageLowerBound

LanguageParameterBounds

LanguageParameters

LanguageParser

LanguageSearchTests

LanguageSlice

MachineBasic

MachineBridge

MachineLanguage

Main

MarkerMixture

MarkerPermutation

MomentBounds

MultiTapeMachine

NormalForm

Restriction

RestrictionClause

RestrictionCorrelation

RestrictionCostCorrelation

RestrictionCountSplit

RestrictionCylinders

RestrictionEasyBase

RestrictionExpansion

RestrictionExpectedCost

RestrictionKeepClause

RestrictionMarkerCNF

RestrictionNormalization

RestrictionPathData

RestrictionPathMixture

RestrictionPathProducts

RestrictionPaths

RestrictionProbability

RestrictionTails

ReversePathEncoding

ReversePathRecurrence

ReversePathWeights

SparseBranch

SparseCorrelation

SparseCounting

SparseFiniteFamily

SparseLeafCNF

SparseLeafCount

SparseNormalize

SparsePartition

SparsePrefix

SparseStreams

SparseTailBounds

SparseTestCodes

SparseThresholds

SparseTree

Substitution

Sunflower

TapeArithmetic

TapeArray

TapeBranch

TapeCancel

TapeCancelRow

TapeCancelStep

TapeConvolutionPrepare

TapeConvolutionRow

TapeConvolutionRows

TapeConvolutionStep

TapeConvolve

TapeCopy

TapeCopyAdd

TapeDecodeBlock

TapeDecodeBlocks

TapeDecodeParsed

TapeDivideFive

TapeEncoding

TapeErase

TapeEvaluation

TapeFill

TapeForLoop

TapeHash

TapeHashClean

TapeHashInitialize

TapeHashInner

TapeHashOuter

TapeHashRow

TapeHashStep

TapeHorner

TapeHornerBody

TapeHornerExtract

TapeHornerLoop

TapeHornerMultiply

TapeHornerPrepare

TapeHornerTake

TapeInitialization

TapeInputBlockLoop

TapeInputBlocks

TapeInputGuard

TapeInputGuardLength

TapeInputPrepare

TapeMultiProgram

TapeMultiRoutines

TapeMultiply

TapeNaturalAccess

TapeOutput

TapeParameterCost

TapeParameterSearch

TapeParameters

TapeParametersBound

TapeParse

TapePower

TapePowerCompare

TapePowerSearch

TapeProductLength

TapeProductTerm

TapeReadPush

TapeRemainder

TapeRemainderOuter

TapeRemainderSetup

TapeRewind

TapeRouting

TapeSearchBody

TapeStoreRepresentation

TapeUnary

TapeUnaryCompare

TapeUnaryCompareScan

TapeWord

TapeWordRewind

TapeXor

ThresholdWeight

TupleCounting

Uniform

UniformSparseBounds

WideCorrelation

Machine (file)

Defs

NormalForm (file)

Defs

Substitution (file)

Defs

Cslib

Defs

ThresholdWeight

Uniform

Defs

Explicit

Encoding (file)

FixedWidth (file)

Codec (file)

Defs

Internal

Conversion (file)

Defs

Internal

Evaluation

Gate (file)

Defs

Internal

Layout (file)

Defs

Internal

Match (file)

Defs

Internal

Output (file)

Defs

Internal

Padded (file)

Defs

Internal

Sequence (file)

Semantics (file)

Defs

Internal

Defs

Internal

Step (file)

Internal

Lookup (file)

Defs

Internal

Validity (file)

Defs

Internal

Defs

Internal

Formula (file)

Batch (file)

Defs

Internal

Stream (file)

Defs

Internal

Defs

Internal

Fragment (file)

Defs

Internal (file)

Codec

Fragment

Semantics

ToCircuit

Machine (file)

Core (file)

Internal

Execution (file)

Gate (file)

Attempt

Loop

LoopReject

Reject

EmptyReject

Family

PositiveLoopReject

PositiveReject

Action

Evaluator

Hoare

Pure

Stage

Tape

Defs

GateStream (file)

Defs

Internal

Internal

FrontEnd

NatCode (file)

Defs

Internal

RawGate (file)

Defs

Internal

Defs

Parity (file)

Defs

Internal

Shift (file)

Defs

Internal

Threshold (file)

Defs

Internal

ToCircuit (file)

Defs

Defs

Family

ExactFourier (file)

Cslib (file)

Defs

Internal

LowerBound

Internal

AmplificationMaster

Boundary

BoundaryActiveCircuit

CascadeLimit

CascadeWord

CircuitCost

CircuitExtensions

ClearedCircuit

ComparisonRename

DiagonalBlocks

DisplacementKernel

FFTCircuit

FiniteSeparation

GraphBlocks

InventoryValidity

LinearDAG

LiveSectors

Main

MatrixRelabel

MonomialFeedback

MonomialTools

MultiWord

PackedSchedule

PairFamilies

ParameterAlgebra

PiTensor

PivotAlgebra

PivotJoin

PolynomialClearing

PortMatrices

PositiveReach

Prices

RationalClearing

RawPositive

RawWordBound

RectStableAlgebra

Shears

SignedPrice

SlotAssembly

SparseShear

SparseSpectral

StreamSeries

SumFramed

SymmetricLaplacian

TensorCostAlgebra

TensorTools

ToeplitzCross

Triangular

WordScheduling

Words

Defs

Family (file)

Defs

FormulaEncoding (file)

Defs

Internal

Frontier (file)

AverageCase

Asymptotics

Bias

Capacity

Circuit

Extractor

Main

Network

Pruning

Sweep

Boundary

Code

Communication

Fiber

Hypergraph

Joint

Linear

MDS

Layouts (file)

BoundedDegree

Compression

Cubic

Gaussian

General

Kernel

Local

Median

MultiCompression

MultiGaussian

MultiGraph

MultiOrder

Probability

Quartic

QuarticCompression

SecondMoment

Star

VertexGaussian

VertexOrder

VertexParameters

Ledger

Aggregate

Basic

Count

LowerBound

Main

Sweep

Linear

Basis

Linearize

LowerBound

Main

TotallyRegular

Tree (file)

Network

AdditiveSweep

Compiler

Components

Cutwidth

Decomposable

Demand

Explicit

Extractor

LowerBound

Main

Multigraph

Network

Nondeterministic

Projection

Rectangle

Reduction

Signals

Sweep

InputPairing (file)

Defs

Internal

InputProjection (file)

Defs

Internal

InputReindexing (file)

Defs

Internal

InputSources (file)

Defs

Internal

Internal

AndOrNot

Bridge

CircuitDescriptor

CircuitToDescriptor

LowerBound

Nondeterminism

NormalForm

Schnorr

SchnorrBridge

SchnorrDeMorgan

ShannonBridge

ShannonUpper

Simulation

Spira

Valiant

KCNF

Internal

Sparsification

Asymptotics

Bounds

Path

Step

Tree

Coding

Isolation

SubcubeFree

Basic

Coding

Defs

Sparsification

SubcubeFree

KarchmerWigderson (file)

Circuit (file)

Internal

Rounds (file)

Defs

Internal

TopDown (file)

Internal

Adversary

Arithmetic

GateBounds

Parity

Rectangle

Sampling

Wires

Majority (file)

Internal

Arithmetic

Bounds

Layers

Neighbors

Defs

Defs

Defs

Internal

KeyedMinimum (file)

Defs

Internal

KeyedMinimumTournament (file)

Family (file)

Defs

Internal

Defs

Internal

Majority (file)

Defs

Internal

Monotone (file)

Defs

Internal

Multiplexer (file)

Defs

Internal

Nondeterminism (file)

Defs

NormalForm (file)

Operations (file)

Defs

Internal

Defs

Restriction

OracleInlining (file)

Adaptive (file)

Defs

Internal

Defs

Internal

RandomRestriction (file)

Defs

Internal

Shallow (file)

Layer (file)

Defs

Internal

Operations

Asymptotic

Bounds

Construction

Covering

Defs

Internal

Moduli

Negations

PairComparison

ShiftTest

Weights

Smolensky (file)

Internal

Binomial

Bound

Circuit

Degree

Gates

Parity

Defs

SparseSynthesis (file)

Internal

Asymptotic

Chunks

Counting

Cover

Estimates

ExtensionBank

Filter

HashCircuit

HashCollision

Intervals

Matrix

Parameters

PartialFinite

PartialTable

SparseFinite

SparseTable

Consequences

Sharpness

Shattering

StraightLine (file)

Defs

Threshold (file)

Parity (file)

Defs

Internal

Defs

Internal

Typed

Defs

Unrolling (file)

Acceptance (file)

Internal

Evaluation

Structure

Defs

Hardwiring

Amplification (file)

Internal

Evaluation

Structure

Topology

Defs

Internal

Initialization

Trace (file)

Internal

Evaluation

HeadBounds

Structure

Topology

Defs

Transition (file)

Fragment (file)

Internal

ArrayEvaluation

Evaluation

Size

Structure

Topology

Defs

Internal

Semantics

Support

Defs

Defs

XOR (file)

Restriction (file)

Defs

Internal

Barrington

BarringtonBridge

BarringtonFamily

BarringtonLength

BarringtonRepr

BarringtonS5

Basic

BitString

BranchingProgram

EssentialInput

Formula

Hardwiring

LowerBound

MultilinearExtension

Restriction

Schnorr

Shannon

Spira

Valiant

Classes (file)

AverageCase (file)

AuxiliaryUnary (file)

Defs

Internal

Ensemble (file)

Defs

Internal

FiniteEnsemble (file)

Defs

Internal

Heuristic (file)

Defs

Internal

Containments (file)

Internal

BinArith

BitCodec

BlockAccept

BlockMember

BlockScan

BlockSearch

BlockSearchCorrect

BoundedReach

CodeAccept

CodeRewind

CodeSearch

CodeStep

ComplementSpace

ConfigCount

ConfigGraph

CountingCert

FPBridge

IPAssemble

IPEnc

IPGameTree

IPLeaf

IPSem

IPStep

IPSubsetPSPACE

IPWalk

InductiveCounting

LogSpaceBound

NLSearchAssemble

PHAssemble

PHAssembleWindow

PHBank

PHBody

PHBodyWindow

PHBounds

PHEmit

PHEpilogue

PHLayout

PHLoop

PHLoopWindow

PHMatrix

PHParts

PHPrologue

PHSubsetPSPACE

PPAssemble

PPBody

PPLayout

PPParts

PPSim

PPSubsetPSPACE

PPTest

PSPACESubsetEXP

PVerdict

PolyWindow

ReachIn

ReachSet

SavitchAssemble

SavitchBits

SavitchBound

SavitchFrame

SavitchReach

SavitchSem

SavitchSim

SavitchStep

SpaceIterate

SuccMachine

TallyLoopIndexed

TranscriptEnc

WitnessEnum

CoNLSubsetNL

Defs

IPSubsetPSPACE

NLSubsetCoNL

NLSubsetP

NPSPACESubsetPSPACE

PHSubsetPSPACE

PPSubsetPSPACE

PSPACESubsetEXP

PSPACESubsetIP

PSPACESubsetNPSPACE

SpaceComplement

FNP (file)

Defs

Internal

L (file)

PolynomialTime (file)

Internal

NP (file)

Internal

Verifier (file)

Linear

Closure

GuessVerify

PairBuildTM

PairSplitTM

VerifierBounds

Verifier (file)

Linear

Closure

CoNP

Reduction

Witness

WitnessConstruction

P (file)

BitPolynomial (file)

Addition (file)

Internal

BlockEval (file)

Internal

Frobenius (file)

Internal

Remainder (file)

Internal

Transpose (file)

Internal

Trinomial (file)

Internal

Internal

Cobham (file)

Internal (file)

Algebra

BlockLoop

BlockScan

Blocks

Cat

ChoiceSim

ConsBit

Encoding

Extract

FstBlock

HeadFlag

Iterate

IterateLayout

MulLen

PolyLen

Reorder

Reverse

Simulate

SndBlock

StepAlgebra

StringOps

TakeLen

Vec

Defs

Vec

DataEncode (file)

Internal

Write

FinsetDomain (file)

Internal

Internal (file)

Composition

NormalForm

Preimage

Iterate (file)

Internal

NatCodes (file)

Internal

PairWithInput (file)

Internal

Range (file)

Defs

Internal

StringAccess (file)

Internal

Unary (file)

Internal

Basic

Bounded

Log

Defs

UnaryLength (file)

Internal

BoundedQuant

Bridge

Composition

DecisionFn

Defs

InitializedIterate

NormalForm

Pairing

Preimage

Verdict

PCP (file)

Internal (file)

AlgCSPModel

AlgCompose

AlgEdge

AlgFamily

AlgFormula

AlgGap

AlgGapAll

AlgGapCSP

AlgGraph

AlgInit

AlgIter

AlgKey

AlgKeyFn

AlgKilled

AlgLevel

AlgLog

AlgPCP

AlgPosNum

AlgPreRel

AlgPreRot

AlgPreprocess

AlgRound

AlgStep

AlgUniform

AlgWalk

AlphabetLift

Amplification

Arithmetize

BaseAlg

BinCounter

BinToUnary

BitwiseFP

BoundNotConstructible

BoundedQuant

CNFCount

CNFMaxVar

CNFSegment

CNFTokens

CSPVerifier

Cheeger

Clique

CloudCount

CloudDisagreement

CoinEnum

Compose

ConsistencyLang

ConstraintGraph

CubeBlocks

DartCorrelation

DataScan

DegreeReduction

DegreeReductionSound

Dinur

Disagreement

EdgeExpansion

Expander

ExpanderExists

ExpanderMerge

ExpanderPad

ExpanderRandom

ExpanderizeCSP

FamilyFin

FiniteKey

FinsetPlurality

GapReduction

GapTheorem

Hadamard

HadamardTester

KilledCSP

KilledFirstMoment

KilledPlurality

KilledWalk

ListEncode

LocalTest

Margulis

Materialize

MaxLoop

MergeGen

Mixing

NatEncode

NumEnc

NumEncPi

PCPtoSAT

Pad

PadGraph

PermArith

PermCount

PermGraph

PosScan

PositionsFP

Power

PoweringBound

Preprocess

RankCount

RegCSP

RegularGraph

SecondMoment

SelfLoops

SquareVerifier

StripTrailing

SubsetNP

SubsetNPFinal

SymbolCodec

TesterChecks

TesterCore

TesterInput

ThreeSATReduction

TowerFin

TowerTable

UnaryDivMod

UnaryExp

UnaryList

Union

VerifierLang

Walk

WalkDart

WalkPath

WalkSplit

ZigZag

ZigZagBaseExists

ZigZagTower

Defs

PH (file)

SipserLautemann (file)

Amplified

Covering

Encode

Matrix

TimeBound

Verdict

PPoly (file)

Advice (file)

Reverse (file)

Defs

Internal

Defs

Internal

Oracle (file)

Evaluation (file)

OutputMatch (file)

Defs

Internal

Defs

Internal

Inlining (file)

Defs

Internal

Defs

Uniform (file)

Containment (file)

Internal

Preprocessing (file)

Defs

Internal

Unrolling (file)

Containment (file)

Internal

Generator

Finalization (file)

Defs

Internal

Initialization (file)

Defs

Internal

Offset (file)

Defs

Internal

PolynomialOffset (file)

Defs

Internal

Primitive (file)

Defs

Internal

Program (file)

Defs

Internal

Tableau (file)

Defs

Internal

Transition

Case (file)

Defs

Internal

Effect (file)

Defs

Internal

MovedHead (file)

Defs

Internal

Next (file)

Defs

Internal

PackedCopy (file)

Defs

Internal

Predecessor (file)

Defs

Internal

Read (file)

Defs

Internal

Step (file)

Internal (file)

Space (file)

Common

Packed

Effect

Emitted

FormulaSpace

Packed

Requires

Sound

Top

Defs

WrittenCell (file)

Defs

Internal

Padded (file)

Defs

Internal

Serializer (file)

Bounds (file)

Defs

Internal

Finalization (file)

Defs

Internal

Initialization (file)

Defs

Internal

Transition (file)

Atomic (file)

Defs

Internal

Case (file)

Defs

Internal

Effect (file)

Defs

Internal

MovedHead (file)

Defs

Internal

Next (file)

Defs

Internal

Polynomial (file)

Defs

Internal

Step (file)

Defs

Internal

WrittenCell (file)

Defs

Internal

Defs

Internal

Defs

Internal

Stream (file)

Defs

Internal

Defs

Internal

Unrolling (file)

Defs

Internal

Defs

Promise (file)

CircuitSize (file)

Defs

Internal

Defs

Internal

Randomized (file)

ApproximateCounting (file)

Internal

ErrorBudget

Power (file)

Defs

Internal

Relative (file)

Circuit (file)

Defs

Internal

OracleProgram (file)

Defs

Internal

Defs

Internal

Weak (file)

Hashing (file)

Defs

Internal

Defs

Internal

Defs

Hashing (file)

Affine (file)

Circuit (file)

Defs

Internal

Defs

Internal

Amplification (file)

Defs

Internal

Defs

Internal

PPoly (file)

Defs

Internal

CircuitAmplification

CircuitHardwiring

GoodSeed

Space (file)

BitstringFold (file)

Defs

Internal

Iterate (file)

Internal

DTISP

EventProb

Exponential

FiniteCounting

Hierarchy

Interactive

Negligible

Pairing

PropertyDensity

SharpP

Time

Cslib

Circuit

Boolean

Correction (file)

Defs

Internal

Complexity

Family

Synthesis

Cut (file)

Defs

Internal

Fanout (file)

Defs

Internal

Complexity

Dependency

Depth

Family

Gated

Program

RelativeComplexity

Synthesis

Upstream

Wire

DescriptiveComplexity (file)

AC0 (file)

Defs

Internal

Circuit (file)

Validity (file)

Defs

Internal

Defs

Encoding

Input

Internal

Encoding (file)

Arithmetic (file)

Defs

Internal

Decoding (file)

Defs

Internal

Positions (file)

Defs

Internal

Validity (file)

Defs

Internal

PolynomialTime

FirstOrder (file)

Blocks

Isomorphism

Semantics

Substitution

Syntax

Interpretation (file)

Composition (file)

Defs

Internal

Pullback (file)

Defs

Internal

Defs

ModelChecking (file)

PolynomialTime (file)

Defs

Internal

Encoded

Numerical (file)

Defs

Internal

Problems

Coloring

Copies

Interpretations

Reduction (file)

Encoding (file)

Defs

Internal

SecondOrder (file)

Certificate (file)

Defs

Internal

Connectives (file)

Defs

Internal

Encoding (file)

Defs

Internal

ModelChecking (file)

Defs

Internal

PolynomialTime (file)

Defs

Internal

Renaming (file)

Defs

Internal

Definable

Isomorphism

Reduction

Semantics

Syntax

TaggedReduction (file)

Encoding (file)

Defs

Internal

Definable

Env

Examples

Isomorphism

Language

Problem

Query

Structure

Vocabulary

Encoding (file)

BitPolynomial (file)

Addition (file)

Defs

Internal

BlockEval (file)

Defs

Internal

Frobenius (file)

Defs

Internal

Remainder (file)

Internal (file)

Step

Width

Defs

Transpose (file)

Defs

Internal

Trinomial (file)

Defs

Internal

Defs

Internal

BinaryNat

Data

DataEncode

DataScan

Delimit

Pairing

Stack

Interop (file)

Cslib (file)

Circuit (file)

Defs

Internal

FromMultiTape (file)

Defs

Internal

PEquiv

MultiTape (file)

Defs

Fun

Internal

Space

CircuitClasses

CircuitDepth

Regular

Mathlib

TM0 (file)

Guard (file)

Defs

Internal

Internal

Initialization

Output

Simulation

Defs

SymbolTracks

Languages (file)

AllSymbol

AnBn

Balanced

Contains

FirstCell

LastBit

LengthDivBy

LengthParity

Palindromes

Trivial

ZeroPrefix

Mathlib

Frontier

SetCard

SimpleGraph

Digraph

FinsetPrefixes

NatBits

Metacomplexity (file)

BooleanDependency (file)

Encoding (file)

Defs

Internal

Defs

Internal

Hamming (file)

Code (file)

Repetition (file)

Defs

Internal

Defs

Internal

Existence (file)

Internal

Defs

Internal

Kolmogorov (file)

Chain (file)

Defs

Internal

Conditional (file)

Defs

Internal

Depth (file)

Defs

Internal

Incompressibility (file)

Defs

Internal

Oracle (file)

Defs

Internal

Symmetry (file)

Defs

Internal

Defs

Internal

ListDecoding (file)

Family (file)

Defs

Internal

Defs

Internal

MCSP (file)

AntiChecker (file)

Approximation (file)

Defs

Internal

Counting (file)

Defs

Internal

Enumeration (file)

FixedWidth (file)

Defs

Internal

Defs

Internal

Extraction (file)

Defs

Internal

GoodString (file)

Circuit (file)

Defs

Internal

Tail (file)

Defs

Internal

Defs

Internal

Rounds (file)

Halving (file)

Internal

Selection (file)

Defs

Internal

Defs

Internal

Selection (file)

Defs

Internal

Defs

Internal

Gap (file)

Slice (file)

Defs

Internal

Defs

Internal

Magnification

AntiChecker (file)

Counter

Circuit (file)

Defs

Internal

Domain (file)

Defs

Internal

Encoding (file)

Defs

Internal

Estimator (file)

Defs

Internal

HashCell (file)

Circuit (file)

Affine (file)

Defs

Internal

Defs

Internal

Defs

Internal

Hashing (file)

Defs

Internal

Randomized (file)

Defs

Internal

Relation (file)

Defs

Internal

Generator (file)

Assembly (file)

Defs

Internal

Iteration (file)

Defs

Internal

Padding (file)

Defs

Internal

Round (file)

Defs

Internal

Selection (file)

Defs

Internal

Size (file)

Defs

Internal

Defs

Internal

GoodString (file)

Internal

Parameters (file)

Defs

Internal

Rounds (file)

Defs

Internal

Frontier (file)

Defs

Internal

Parameters (file)

Defs

Internal

Normalization (file)

Defs

Internal

Raw (file)

Defs

Internal

Shannon (file)

Internal

Succinct (file)

NP (file)

Defs

Internal

Normalization (file)

Defs

Internal

Witness (file)

Defs

Internal

Defs

Internal

Threshold (file)

Defs

Internal

Witness (file)

Defs

Internal

Defs

Internal

MINCKT (file)

Gap (file)

Difference (file)

SoI (file)

Unconditional (file)

Efficient (file)

Defs

Internal

Final (file)

Internal

Growth (file)

Internal

Iterated (file)

Defs

Internal

Slack (file)

Defs

Internal

Consequence

Defs

Internal

Defs

Internal

Defs

Internal

Multiplicative (file)

Defs

Internal

Defs

Internal

Defs

Internal

MINKT (file)

AuxiliaryUnary (file)

Defs

Internal

Gap (file)

Logarithmic (file)

Efficient (file)

Defs

Internal

Defs

Internal

Defs

Internal

Defs

Internal

NisanWigderson (file)

Encoding (file)

Defs

Internal

Hardwiring (file)

Defs

Internal

Reconstruction (file)

Averaging (file)

Defs

Internal

CertificateSearch (file)

Defs

Internal

GlobalSampling (file)

Defs

Internal

Program (file)

Encoding (file)

Defs

Internal

ListDecoding (file)

Family (file)

Defs

Internal

Defs

Internal

Defs

Internal

RepeatedSampling (file)

Defs

Internal

Defs

Internal

Defs

Internal

ScaledExponent (file)

Defs

Internal

StatisticalTest (file)

Hybrid (file)

Defs

Internal

HybridPrediction (file)

Defs

Internal

Oracle (file)

Defs

Internal

Prediction (file)

Defs

Internal

Defs

Internal

Models (file)

FiniteAutomaton

Complementation (file)

Internal

Amplification

Bridge

Chain

Classes

Corners

Diagram

Encoding

ImageBound

Main

Model

Nesting

Network

Normalization

Recognition

RelationMonoid

Relations

Representation

Retained

Source

Tape

Transport

OneWayLiveness (file)

Binary (file)

Defs

Internal

Binary

Cells

Corners

Diagram

Diagrams

Encoding

Main

Model

NFABridge

Network

Normalization

PathNFA

Rank

RankLoss

Recognition

Relations

Syntactic

Tours

Wiring

Defs

Encoding

Defs

RandomAccessMachine (file)

Classes (file)

Defs

Simulation

RegisterStore (file)

Containment (file)

Defs

Internal

DenseOverlay (file)

Defs

Internal

Machine

AddressEq (file)

Defs

Internal

DenseInputLookup (file)

Defs

Internal

EntryAppend (file)

Defs

Internal

EntryCleanup (file)

Defs

Internal

EntryDecode (file)

Defs

Internal

LinearInternal

EntryEncode (file)

Defs

Internal

EntryLookup (file)

Defs

Internal

EntryMatch (file)

Defs

Internal

EntryMissCopy (file)

Defs

Internal

EntryReplace (file)

Defs

Internal

EntryScan (file)

Internal

Bounds

Ctrl

Inv

Sem

Defs

EntryScanStep (file)

Defs

Internal

EntryUpdate (file)

Internal

Ctrl

End

Hit

Inv

Loop

Miss

Out

Sem

Step

Time

BoundsInternal

Defs

Progress

Source

Tagged

TaggedDefs

TaggedProof

Instruction (file)

Sim

Control

Data

Defs

Internal

Control

Defs

Dense

DenseControl

DenseCtrlSim

DenseDefs

DenseDirect

DenseDispatch

DenseImm

DenseLoad

DenseSim

DenseSimData

DenseSimDefs

DenseStore

Direct

Dispatch

Immediate

Internal

Load

Store

Lookup

Internal

Assemble

Bounds

Prepare

Reset

Restore

Scan

Static

Value

Defs

DenseInternal

Program (file)

Bounds (file)

Defs

Internal

Decision (file)

Defs

Init

Defs

Internal

DecisionInternal

Defs

Dense

DenseBounds

DenseBoundsDefs

DenseBoundsProof

DenseDecision

DenseDecisionDefs

DenseDecisionProof

DenseDefs

DenseInit

DenseInitDefs

DenseInitProof

DenseInternal

Initialization

Internal

WordDecode (file)

Defs

Internal

LinearInternal

WordEncode (file)

Defs

Internal

EntryLookupRestore

Defs

Internal

TMConfig (file)

Sparse (file)

ABI (file)

Internal

Capture

Decision

Loop

Marshal

Resources

Defs

Containment (file)

Internal

Step (file)

Internal (file)

Action

Dispatch

Iteration

Layout

Load

Resources

Defs

Defs

Internal

Step (file)

Internal (file)

Action

Dispatch

Layout

Load

Resources

Defs

Defs

Internal

Structured (file)

GateEval (file)

Defs

Internal

GateStep (file)

Defs

Internal

GateStreamStep (file)

Defs

Internal

Hamming (file)

Defs

Internal

Internal (file)

Resources

LastBit (file)

Defs

PairValidate (file)

Defs

Internal

Scanner (file)

Defs

Internal

Switch (file)

Compiled

Defs

Internal

ThreeSATSyntax (file)

Defs

UnaryDecode (file)

Defs

Internal

Defs

Defs

Internal

Soundness

RoseTreeMachine

Prog

TuringMachine (file)

Combinators (file)

ForBinaryWork (file)

Defs

Internal

ForInput (file)

Defs

Internal

ForWorkOnes (file)

Defs

Internal

Internal (file)

Complement

Generic

IdleHeads

If

Loop

LoopIndexed

LoopIteration

Retarget

RetargetWindow

Scanner

SentinelStep

Seq

SeqChain

Union

Window

RetargetCompute (file)

Defs

Internal

WorkBranch (file)

Defs

Internal

WorkSymbolBranch (file)

Defs

Internal

Apply

ApplyDecide

Composition (file)

Internal (file)

FirstPhase

NondetPlaced

NondetPrefix

Tail

Nondeterministic (file)

Decides

Trace

PairWithInput (file)

Defs

Internal

Defs

Experimental

BinaryRoutine (file)

Arithmetic (file)

Defs

Internal

Control (file)

Defs

Internal

InputLength (file)

Defs

Internal

List (file)

Defs

Internal

SpaceBounds (file)

Defs

Internal

Defs

Internal

Routine (file)

Defs

Internal

EmitSpec

Hoare (file)

Safety (file)

Defs

Internal

Space (file)

Defs

Internal

Defs

RetargetOutput

SpaceFrame

StartInvariant

Internal (file)

OutputBounds

Lift (file)

Hoare

Oracle (file)

OutputSemantics (file)

Defs

Internal

Universality (file)

Defs

Internal

Defs

Internal

OutputSemantics (file)

Defs

Internal

Placement (file)

Defs

Hoare

Internal

Window

Registers (file)

Arith

DecReg

Emit

EmitSeq

ForReg

Horner

InputLen

MixedRadix

Probe

RegisterOps

Repetition (file)

Internal (file)

Boundary

Correctness

Finish

Frame

Parked

Rewind

Schedule

ScheduleArithmetic

Setup

Trial

VoteStep

Votes

Correctness

Defs

SingleTape (file)

Internal (file)

Correctness

Delta

Pad

Sim

SpaceTime (file)

Internal

Observation

OutputFrontier

Reachability

RunBound

Snapshot

Defs

Subroutines (file)

BinaryAdd (file)

Defs

Internal

BinaryAddConst (file)

Defs

Internal

BinaryBump (file)

Defs

Internal

BinaryCopy (file)

Defs

Internal

BinaryEq (file)

Defs

Internal

BinaryFor (file)

Internal (file)

Comparison

Control

Hoare

Loop

Defs

BinaryLength (file)

Defs

Internal

BinaryMulAdd (file)

Defs

Internal

BinaryPolynomial (file)

Defs

Internal

BinaryPred (file)

Defs

Internal

BinaryRippleAdd (file)

Internal (file)

Bounds

Out

Pure

Rewind

Scan

Sem

Defs

BinaryRippleSub (file)

Internal

Backward

Out

Pure

Rewind

Scan

Sem

Defs

BinaryShiftMul (file)

Internal

Out

Pure

Sem

Defs

BinarySucc (file)

Defs

Internal

ClearWork (file)

Defs

Internal

Internal (file)

CopyOutput

CopyWorkOutput

ScanRight

PairEmit (file)

Defs

Internal

PairSplit (file)

Defs

Internal

PairValidate (file)

Defs

Internal

ResetBinary (file)

Defs

Internal

ResetBinaryMany (file)

Defs

Internal

UnaryLength (file)

Defs

Internal

CopyOutput

CopyToVirtualInput

CopyWorkOutput

Counter

GuessBounded

InputMatch

MoveLeftStep

PairBuild

ParkAll

ParkRewind

ResetTapes

RewindList

Scan

ScanRight

WipeLoop

WipeRewind

WipeStep

WriteOutputBit

Tape

Encoding

Trace (file)

DetPrefix

Internal

UTM

Internal

Body

BodyApply

BodyAssembly

BodyInternal

BodyIteration

BodyLookup

BodyLoop

BodyMatch

ClockFrontier

Desc

DescLayout

Extract

HaltTest

Init

Interp

NegOut

PairSelf

SeekFrontier

Sim

SimClocked

SimLoop

StepGlue

TermCheck

Terminated

Universality

VTape

Verdict

Clock

ClockConstructible

ClockedUtm

Diagonal

Encoding

HierarchySupport

Machine

Universal

Universality

Universality (file)

Defs

Internal

Witness (file)

BoundSetup (file)

Defs

Internal

Reserved

Store (file)

Defs

Internal

Verifier (file)

Internal (file)

Join

Pair

Prefix

Run

Suffix

Defs

Defs

Internal

PhaseSafety

Branch

ChoiceTape

Delay

Deterministic

Frame

GuessAssembly

GuessStream

GuessTape

OutputBounds

Transport

WorkReadOnly

RationalHitting (file)

Evaluation (file)

Defs

Internal

Affine

BinaryAddition

BinaryBinomial

BinaryDivision

BinaryFactorial

BinaryGcd

BinaryMultiply

BinarySubtract

BinomialBounds

BlockDivision

Certificates

Compiler

CyclotomicGrid

Deformation

DenseDeterminant

DenseRecords

Detection

Determinant

EncodingBounds

Evaluation

Executable

Feasibility

FiniteCompiler

Generator

GridComputation

InputAdapter

IntegralLift

LaurentReduction

LiftComputation

ListProcedures

Main

MatrixComputation

OutputAdapter

OutputComputation

PaddedRank

ProcedureControl

ProcedurePairs

Procedures

QuantumMatrices

QuantumSeries

RationalArithmetic

RationalBinary

Rectangular

SignedArithmetic

SignedBinary

SmallExpansion

StackLanguage

StackSimulation

StackWords

Tabulation

TaylorComputation

UnaryArithmetic

Wronskian

PolynomialTime (file)

Defs

Internal

Defs

SAT (file)

CircuitSatisfiability (file)

Defs

Internal

CookLevin (file)

Internal

Emitter

EmitterActive

EmitterFamilies

EmitterLoop

EmitterStart

Assembly

Corollaries

Internal

GuessVerify

LinearGuessVerify

ThreeSAT (file)

Completeness

Headline

Syntax

Verifier

Tseitin (file)

Internal

Correctness

EncodingBounds

FunctionSemantics

Shape

Size

StateBounds

Streaming

StreamingEndpoint

Machine (file)

Internal

BranchFrame

BufferSpecs

ControllerCalls

ControllerInput

ControllerInvariant

ControllerLift

ControllerRead

ControllerRun

ControllerSemantics

ControllerToken

EmitterSpec

FrontEndSpec

InvalidBranchSpec

PolynomialTime

RuntimeBounds

Setup

ValidBranchAssembly

Validation

ValidationFramed

Controller

Defs

Defs

CircuitOracle

Encoding

GuessVerify

Headline

Language

QBF

Rename

Resolution

Semantics

ThreeCNF

Verifier

VerifierTM

Tactic

PolyTime (file)

Init

TimeConstructible

Cslib

Computability

Automata

Acceptors

Acceptor

OmegaAcceptor

DA

Basic

Congr

Prod

ToNA

NA

Basic

Concat

Loop

Preimage

Reverse

ToDA

Total

TwoWayNA

Basic

ComplToNA

OfNA

Circuit

Boolean

Basic

Counting

Lupanov

LupanovConstruction

Shannon

Synthesis

Basic

Complexity

Composition

Counting

Finite

Homomorphism

Normalization

Program

Shannon

Signature

Synthesis

Wire

Languages

Congruences

Basic

MyhillCongruence

Language

LanguageHom

MyhillNerode

OmegaLanguage

RegularLanguage

Slice

SyntacticMonoid

Machines

Turing

MultiTape

Configuration

Deterministic

Foundations

Data

List

IsChainFromTo

Nat

Asymptotics

Factorial

Segment

OmegaSequence

Defs

Flatten

InfOcc

Init

Temporal

Topology

BitString

Lint

Basic

Relation

Defs

RelatesInSteps

Semantics

FLTS

Basic

FLTSToLTS

LTSToFLTS

Prod

LTS

Basic

Execution

MapHom

OmegaExecution

Relation

Reverse

Total

Tactic

GrindAttrs

Init

ImportGraph

Graph

TransitiveClosure

Imports

FromSource

ImportGraph

Pretty

Redundant

RequiredModules

Lean

EnvExtension

Environment

Json

MessageData

Syntax

Shake

Algebra

Basic

Core

DeclNeeds

EnvExtension

Environment

Workspace

Tools (file)

FindHome

ImportDiff

MinImports

NormImports

RedundantImports

Widget

Collapsible

Copy

GoToModule

WorkspaceModel

Summary (file)

Core

Get

Lake

Base

Build

Model

Lake

Init (file)

Control (file)

Lawful (file)

MonadAttach (file)

Instances

Lemmas

MonadLift (file)

Basic

Instances

Lemmas

Basic

Instances

Lemmas

Basic

Do

EState

Except

ExceptCps

Id

MonadAttach

Option

Reader

State

StateCps

StateRef

Data (file)

Array (file)

Lex (file)

Basic

Lemmas

QSort (file)

Basic

Sort (file)

Basic

Lemmas

Subarray (file)

Split

Attach

Basic

BasicAux

BinSearch

Bootstrap

Count

DecidableEq

Erase

Extract

FinRange

Find

GetLit

InsertIdx

InsertionSort

Int

Lemmas

MapIdx

Mem

MinMax

Monadic

Nat

OfFn

Perm

Range

Set

TakeDrop

Zip

BitVec (file)

Basic

BasicAux

Bitblast

Bootstrap

Decidable

Folds

Lemmas

ByteArray (file)

Basic

Bootstrap

Extra

Lemmas

Char (file)

Basic

Lemmas

Order

Ordinal

Dyadic (file)

Basic

Instances

Inv

Round

Fin (file)

Basic

Bitwise

Fold

Iterate

Lemmas

Log2

MinMax

OverflowAware

Package

Float (file)

Model (file)

Format (file)

Basic

Valid

Unpacked (file)

Operations (file)

Add

Compare

Div

Fma

Mul

OfNat

OfScientific

Sign

Sqrt

Status

Sub

ToNat

Pack (file)

Basic

Lemmas

Basic

Round

Sign

Float

Float32

Float

Float32

FloatArray (file)

Basic

Format (file)

Basic

Instances

Macro

Syntax

Int (file)

Bitwise (file)

Basic

Lemmas

DivMod (file)

Basic

Bootstrap

Lemmas

Pow

Basic

Compare

Cooper

Gcd

Lemmas

LemmasAux

Linear

OfNat

Order

Package

Pow

Repr

ToString

Iterators (file)

Combinators (file)

Monadic (file)

Append

Attach

FilterMap

FlatMap

Take

ULift

Append

Attach

FilterMap

FlatMap

Take

ULift

Consumers (file)

Monadic (file)

Access

Collect

Loop

Partial

Total

Access

Collect

Loop

Partial

Stream

Total

Internal (file)

LawfulMonadLiftFunction

Lemmas (file)

Combinators (file)

Monadic (file)

Append

Attach

FilterMap

FlatMap

Take

ULift

Append

Attach

FilterMap

FlatMap

Take

ULift

Consumers (file)

Monadic (file)

Collect

Loop

Access

Collect

Loop

Monadic

Basic

Producers (file)

Monadic (file)

List

List

Basic

Producers (file)

Monadic (file)

List

List

Basic

PostconditionMonad

ToIterator

List (file)

Int (file)

Prod

Sum

Nat (file)

BEq

Basic

Count

Erase

Find

InsertIdx

Modify

Pairwise

Perm

Prod

Range

Sublist

Sum

TakeDrop

Scan (file)

Basic

Lemmas

Sort (file)

Basic

Impl

Lemmas

SplitOn (file)

Basic

Lemmas

Attach

Basic

BasicAux

Control

ControlImpl

Count

Erase

FinRange

Find

Impl

Lemmas

Lex

MapIdx

MinMax

MinMaxIdx

MinMaxOn

Monadic

Notation

OfFn

Pairwise

Perm

Range

Sublist

TakeDrop

ToArray

ToArrayImpl

Zip

Nat (file)

Bitwise (file)

Basic

Lemmas

Div (file)

Basic

Lemmas

Internal (file)

Linear

SOM

Power2 (file)

Basic

Bitwise

Lemmas

Sqrt (file)

Basic

Lemmas

Basic

Compare

Control

Coprime

Dvd

Fold

Gcd

Lcm

Lemmas

Log2

MinMax

Mod

Order

Package

PowMod

Simproc

ToString

OfScientific (file)

Basic

Option (file)

Array

Attach

Basic

BasicAux

Coe

Function

Instances

Lemmas

List

Monadic

Ord (file)

Array

Basic

BitVec

SInt

String

UInt

Vector

Order (file)

Classes

ClassesExtra

Factories

FactoriesExtra

Lemmas

LemmasExtra

MinMaxOn

Opposite

Ord

PackageFactories

Range (file)

Polymorphic (file)

Internal

SignedBitVec

Basic

BitVec

Char

Fin

GetElemTactic

Instances

Int

IntLemmas

Iterators

Lemmas

Map

Nat

NatLemmas

PRange

RangeIterator

SInt

Stream

UInt

UpwardEnumerable

Basic

Lemmas

Rat (file)

Basic

Lemmas

SInt (file)

Basic

Bitwise

Float

Float32

IntToBitVec

Lemmas

Package

Slice (file)

Array (file)

Basic

Iterator

Lemmas

List (file)

Basic

Iterator

Lemmas

Basic

InternalLemmas

Lemmas

Notation

Operations

String (file)

Iter (file)

Basic

Intercalate

Lemmas (file)

Pattern (file)

Find (file)

Basic

Char

Pred

String

Split (file)

Basic

Char

Pred

String (file)

Basic

ForwardPattern

ForwardSearcher

TakeDrop (file)

Basic

Char

Pred

String

Basic

Char

Memcmp

Pred

Basic

FindPos

Hashable

Intercalate

IsEmpty

Iter

Iterate

Length

Modify

Order

Search

Slice

Splits

StringOrder

TakeDrop

Pattern (file)

Basic

Char

Pred

String

Basic

Bootstrap

Decode

Defs

Extra

FindPos

Hashable

Iterate

Iterator

Legacy

Length

Modify

OrderInstances

PosRaw

Search

Slice

Stream

Subslice

Substring

TakeDrop

Termination

ToSlice

Subtype (file)

Basic

Order

OrderExtra

Sum (file)

Basic

Lemmas

ToString (file)

Basic

Extra

Macro

Name

UInt (file)

Basic

BasicAux

Bitwise

IntToBitVec

Lemmas

Log2

Package

Vector (file)

Algebra

Attach

Basic

Count

DecidableEq

Erase

Extract

FinRange

Find

InsertIdx

Int

Lemmas

Lex

MapIdx

Monadic

Nat

OfFn

Perm

Range

Stream

Zip

AC

BEq

Bool

Cast

Erased

Function

Hashable

LawfulHashable

NeZero

PLift

Prod

Queue

RArray

Random

Repr

Stream

ULift

Zero

Grind (file)

Homo (file)

BitVec

Extra

Fin

ISize

Int16

Int32

Int64

Int8

UInt16

UInt32

UInt64

UInt8

USize

Module (file)

Basic

Envelope

NatModuleNorm

OfNatModule

Ordered (file)

Field

Int

Linarith

Module

Order

Rat

Ring

Ring (file)

Basic

CommSemiringAdapter

CommSolver

Envelope

Field

OfScientific

AC

Annotated

Attr

Cases

Config

Ext

FieldNormNum

Injective

Interactive

Lemmas

Lint

Norm

Offset

Order

PP

Propagator

Tactics

ToInt

Util

GrindInstances (file)

Ring (file)

BitVec

Fin

Int

Nat

Rat

SInt

UInt

Nat

Internal (file)

Order (file)

Basic

Lemmas

MonadTail

Tactic

While

Meta (file)

Defs

Omega (file)

Coeffs

Constraint

Int

IntList

LinearCombo

Logic

Sym (file)

DSimp

DSimprocDSL

Simp

SimprocDSL

Lemmas

System (file)

CancelToken

FilePath

IO

IOError

Platform

Promise

ST

Uri

BinderNameHint

BinderPredicates

ByCases

CbvSimproc

Classical

Coe

Conv

Core

Dynamic

Ext

GetElem

Guard

Hints

LawfulBEqTactics

LetFun

MacroTrace

MetaTypes

MethodSpecsSimp

Notation

NotationExtra

Prelude

PropLemmas

RCases

ShareCommon

SimpLemmas

Simproc

SizeOf

SizeOfLemmas

Syntax

Tactics

TacticsExtra

Task

Try

Util

WF

WFComputable

WFExtrinsicFix

WFTactics

While

Lake (file)

Build (file)

Job (file)

Basic

Monad

Register

Target (file)

Basic

Fetch

Actions

Common

Context

Data

Executable

ExternLib

Facets

Fetch

Index

Info

Infos

InitFacets

InputFile

Key

Library

Module

ModuleArtifacts

Package

Run

Store

Targets

Topological

Trace

CLI

Actions

Config (file)

Artifact

Cache

ConfigDecl

ConfigTarget

Context

Defaults

Dependency

Dynlib

Env

ExternLib

ExternLibConfig

FacetConfig

Glob

InputFile

InputFileConfig

InstallPath

Kinds

LakeConfig

Lang

LeanConfig

LeanExe

LeanExeConfig

LeanLib

LeanLibConfig

Meta

MetaClasses

Module

Monad

Opaque

OutFormat

Package

PackageConfig

Pattern

Script

TargetConfig

Workspace

WorkspaceConfig

DSL (file)

Attributes

AttributesCore

Config

DeclUtil

Extensions

Key

Meta

Package

Require

Script

Syntax

Targets

VerLit

Load

Workspace

Toml (file)

Data (file)

DateTime

Dict

Value

Elab (file)

Expression

Value

Decode

Encode

Grammar

Load

ParserUtil

Util (file)

Binder

Casing

Cli

Cycle

Date

EStateT

EquipT

Error

Exit

Family

FilePath

Git

IO

JsonObject

Lift

Lock

Log

MainM

Message

Name

NativeLib

Opaque

OpaqueType

OrdHashSet

OrderedTagAttribute

Proc

RBArray

Reservoir

Store

StoreInsts

String

Task

Url

Version

Reservoir

Version

Lean (file)

Compiler (file)

IR (file)

Basic

Checker

CompilerM

EmitLLVM

EmitUtil

Format

LLVMBindings

Meta

NormIds

Sorry

ToIR

ToIRType

UnboxResult

LCNF (file)

Simp (file)

Basic

Config

ConstantFold

DefaultAlt

DiscrM

FunDeclInfo

InlineCandidate

InlineProj

JpCases

Main

SimpM

SimpValue

Used

AlphaEqv

AuxDeclCache

BaseTypes

Basic

Bind

CSE

Check

Closure

CoalesceRC

CompatibleTypes

CompilerM

ConfigOptions

DeclHash

DependsOn

ElimDead

ElimDeadBranches

EmitC

EmitUtil

ExpandResetReuse

ExplicitBoxing

ExplicitRC

ExtractClosed

FVarUtil

FixedParams

FloatLetIn

InferBorrow

InferType

Internalize

Irrelevant

JoinPoints

LCtx

LambdaLifting

Level

LiveVars

Main

MonadScope

MonoTypes

OtherDecl

PassManager

Passes

PhaseExt

PrettyPrinter

Probing

PropagateBorrow

PublicDeclsExt

PullFunDecls

PullLetDecls

PushProj

ReduceArity

ReduceJpArity

Renaming

ResetReuse

ScopeM

SimpCase

SimpleGroundExpr

SpecInfo

Specialize

SplitSCC

StructProjCases

ToDecl

ToExpr

ToImpure

ToImpureType

ToLCNF

ToMono

Toposort

Types

Util

Visibility

BorrowedAnnotation

CSimpAttr

ClosedTermCache

ExportAttr

ExternAttr

FFI

ImplementedByAttr

InitAttr

InlineAttrs

Main

MetaAttr

ModPkgExt

NameDemangling

NameMangling

NeverExtractAttr

NoncomputableAttr

Old

Options

Specialize

Data (file)

Iterators (file)

Producers (file)

PersistentHashMap

Json (file)

FromToJson (file)

Basic

Extra

Basic

Elab

Parser

Printer

Stream

Lsp (file)

Basic

BasicAux

CancelParams

Capabilities

Client

CodeActions

Communication

Diagnostics

Extra

InitShutdown

Internal

Ipc

LanguageFeatures

TextSync

Utf16

Window

Workspace

NameMap (file)

AdditionalOperations

Basic

Array

AssocList

DeclarationRange

EditDistance

Format

FuzzyMatching

JsonRpc

KVMap

LBool

LOption

Name

NameTrie

OpenDecl

Options

PPContext

PersistentArray

PersistentHashMap

PersistentHashSet

Position

PrefixTree

RArray

RBMap

RBTree

SMap

SSet

Trie

DocString (file)

Add

DeferredCheck

Extension

Formatter

Links

Markdown

Parser

Syntax

Types

Elab (file)

BuiltinDo (file)

Basic

For

Forward

If

Jump

Let

Match

MatchExpr

Misc

Repeat

TryCatch

Command (file)

Scope

WithWeakNamespace

ConfigEval (file)

Basic

Builtins

Commands

DeriveEvalConfigItem

DeriveEvalExpr

DeriveEvalTerm

Extra

Instances

MetaInstances

Types

Util

Deriving (file)

BEq

Basic

DecEq

FromToJson

Hashable

Inhabited

LawfulBEq

Nonempty

Ord

ReflBEq

Repr

SizeOf

ToExpr

TypeName

Util

Do (file)

Basic

Control

ForwardSyntax

InferControlInfo

Legacy

PatternVar

Switch

DocString (file)

Builtin (file)

Keywords

Parsing

Postponed

Scopes

InfoTree (file)

Basic

InlayHints

Main

Types

Util

PreDefinition (file)

PartialFixpoint (file)

Eqns

Induction

Main

Structural (file)

BRecOn

Basic

Eqns

FindRecArg

IndGroupInfo

IndPred

Main

Preprocess

RecArgInfo

SmartUnfolding

WF (file)

Basic

Eqns

Fix

FloatRecApp

GuessLex

Main

PackMutual

Preprocess

Rel

Unfold

Basic

EqUnfold

Eqns

EqnsUtils

FixedParams

Main

MkInhabitant

Mutual

TerminationHint

TerminationMeasure

Quotation (file)

Precheck

Util

Tactic (file)

Conv (file)

Basic

Cbv

Change

Congr

Delta

Lets

Pattern

Rewrite

Simp

Unfold

Do (file)

ProofMode (file)

Assumption

Basic

Cases

Clear

Constructor

Delab

Exact

Exfalso

Focus

Frame

Have

Intro

LeftRight

MGoal

Pure

Refine

RenameI

Revert

Specialize

VCGen (file)

Basic

Split

SuggestInvariant

Attr

ConjunctivePre

Contract

LetElim

Spec

Syntax

Grind (file)

Anchor

Annotated

BVDecide

Basic

BuiltinTactic

Cbv

Config

DSimp

DSimprocDSL

DSimprocDSLBuiltin

Filter

Have

LetToHave

LiftLet

Lint

LintExceptions

Main

Param

RegisterSymDSimp

RegisterSymSimp

Rewrite

ShowState

SimprocDSL

SimprocDSLBuiltin

Sym

Trace

WithGrindTacticM

Omega (file)

Core

Frontend

MinNatAbs

OmegaM

VCGen (file)

BinderName

Context

Driver

Entails

FrameProc

FrameProcAttr

Frontend

LatticeOp

Reduce

RuleCache

RuleConstruction

Solve

SpecDB

Util

WPApp

AsAuxLemma

AutoTry

BVDecide

Basic

BoolToPropSimps

BuiltinTactic

Calc

Cbv

CbvSimproc

Change

Classical

Config

Congr

Decide

Delta

DiscrTreeKey

Doc

ElabTerm

ExposeNames

Ext

FalseOrByContra

Generalize

Guard

Impossible

Induction

Injection

Lets

LibrarySearch

Location

Match

Meta

Monotonicity

NormCast

RCases

RenameInaccessibles

Repeat

Rewrite

Rewrites

Rfl

Rwa

Show

ShowTerm

Simp

SimpArith

SimpTrace

Simpa

Simproc

SolveByElim

Split

Symm

TreeTacAttr

Try

Unfold

Term (file)

TermElabM

App

Arg

AssertExists

Attributes

AutoBound

AuxDef

BinderPredicates

Binders

BindersUtil

BuiltinCommand

BuiltinEvalCommand

BuiltinNotation

BuiltinTerm

Calc

CheckTactic

Coinductive

ComputedFields

Config

DeclModifiers

DeclNameGen

DeclUtil

Declaration

DeclarationRange

DefView

DeprecatedArg

DeprecatedSyntax

ElabRules

ErrorExplanation

ErrorUtils

Eval

Exception

Extra

Frontend

GenInjective

GuardMsgs

Idbg

Import

Inductive

InfoTrees

InheritDoc

LetRec

Level

Macro

MacroArgUtil

MacroRules

Match

MatchAltView

MatchExpr

Mixfix

MutualDef

MutualInductive

Notation

Open

Parallel

ParseImportsFast

PatternVar

Print

RecAppSyntax

Recall

RecommendedSpelling

SetOption

StructInst

StructInstHint

Structure

Syntax

SyntheticMVars

Task

Time

Util

WhereFinally

Language

Lean (file)

Types

Util

Basic

Util

LibrarySuggestions (file)

Basic

Default

MePo

SineQuaNon

SymbolFrequency

Linter (file)

CodeQuality (file)

Basic

Frontend

EnvLinter (file)

Basic

Frontend

Extra (file)

DupNamespace

UnnecessarySeqFocus

UnreachableTactic

UnusedDecidableInType

AmbiguousOpen

Basic

Builtin

CheckUnivs

Coe

ConstructorAsVariable

CoreInternal

DefProp

Deprecated

DocsOnAlt

GlobalAttributeIn

Init

InternalModule

List

MissingDocs

Omit

PersistentLintLog

Sets

TacticTypeCheck

UnusedSimpArgs

UnusedVariables

Util

Meta (file)

ArgsPacker (file)

Basic

Constructions (file)

BRecOn

CasesOn

CasesOnSameCtor

CtorElim

CtorIdx

NoConfusion

RecOn

SparseCasesOn

SparseCasesOnEq

DiscrTree (file)

Basic

Main

Types

Util

Match (file)

MatcherApp (file)

Basic

Transform

AltTelescopes

Basic

CaseArraySizes

CaseValues

MVarRenaming

Match

MatchEqs

MatchEqsExt

MatchPatternAttr

MatcherInfo

NamedPatterns

Rewrite

SimpH

SolveOverlap

Value

Sym (file)

Arith (file)

Classify

DenoteExpr

EvalNum

Functions

MonadCanon

MonadRing

MonadSemiring

MonadVar

Poly

Reify

ToExpr

Types

VarRename

DSimp (file)

App

DSimpM

DSimproc

EvalGround

Forall

Lambda

Let

Main

Reduce

Result

Variant

Simp (file)

App

Attr

CongrInfo

ControlFlow

Debug

Discharger

DiscrTree

EvalGround

Forall

Goal

Have

Lambda

Main

RegisterCommand

Result

Rewrite

SimpM

Simproc

Telescope

Theorems

Variant

AbstractS

AlphaShareBuilder

AlphaShareCommon

Apply

Canon

Eta

ExprPtr

Grind

InferType

InstantiateMVarsS

InstantiateS

Intro

IsClass

LetToHave

LiftLet

LitValues

LooseBVarsS

MaxFVar

Offset

Pattern

ProofInstInfo

ReplaceS

SymM

SynthInstance

Util

Tactic (file)

AC (file)

Main

BVDecide (file)

LRAT (file)

Cert

Trim

Normalize (file)

AC

AndFlatten

ApplyControlFlow

Basic

CollectHyps

EmbeddedConstraint

Enums

IntToBitVec

Reduction

Rewrite

ShortCircuit

Simproc

Structures

TypeAnalysis

Prover (file)

Basic

Bitblast

Reflect (file)

Basic

ReifiedBVExpr

ReifiedBVLogical

ReifiedBVPred

ReifiedLemmas

Reify

SatAtBVLogical

Attr

Counterexample

External

Main

TacticContext

Cbv (file)

BuiltinCbvSimprocs

Array

Core

String

CbvEvalExt

CbvSimproc

ControlFlow

Main

Opaque

TheoremsLookup

Util

Grind (file)

AC (file)

Action

DenoteExpr

Eq

Internalize

Inv

PP

Proof

Seq

ToExpr

Types

Util

Var

VarRename

Arith (file)

CommRing (file)

Action

DenoteExpr

EqCnstr

Functions

Internalize

Inv

MonadRing

MonadSemiring

NonCommRingM

NonCommSemiringM

PP

Power

Proof

Reify

RingId

RingM

SafePoly

SemiringM

Types

Cutsat (file)

Action

CommRing

DvdCnstr

EqCnstr

Inv

LeCnstr

MBTC

Model

Nat

Norm

Proof

ReorderVars

Search

SearchM

Types

Util

Var

VarRename

Linear (file)

Action

Den

DenoteExpr

IneqCnstr

Internalize

Inv

LinearM

MBTC

Model

OfNatModule

PP

Proof

PropagateEq

Reify

Search

SearchM

StructId

ToExpr

Types

Util

Var

VarRename

EvalNum

FieldNormNum

Insts

IsRelevant

Main

Model

ModelUtil

Propagate

Simproc

Types

Util

BVDecide (file)

Types

Order (file)

Assert

Internalize

OrderM

Proof

StructId

Types

Util

Action

Anchor

Attr

Beta

BitVec

Cases

CasesMatch

CastLike

CheckResult

CollectParams

Core

Ctor

CtorIdx

Diseq

EMatch

EMatchAction

EMatchDiagnostics

EMatchTheorem

EMatchTheoremParam

EMatchTheoremPtr

EqResolution

Ext

ExtAttr

Extension

Filter

Finish

ForallProp

Homo

Homomorphism

Injection

Injective

Internalize

Intro

Inv

LawfulEqCmp

Lookahead

MBTC

Main

MarkAccessible

MarkNestedSubsingletons

MatchCond

MatchDiscrOnly

OrderInsts

PP

Parser

Proj

Proof

ProofUtil

Propagate

PropagateInj

PropagatorAttr

ProveEq

ReflCmp

RegisterCommand

Simp

SimpUtil

Solve

Split

SynthInstance

Theorems

Types

Util

VarRename

Simp (file)

Arith (file)

Int (file)

Basic

Simp

Nat (file)

Basic

Simp

Util

BuiltinSimprocs (file)

Array

BitVec

Char

Core

CtorIdx

Fin

Int

List

MethodSpecs

Nat

SInt

String

UInt

Util

Attr

Diagnostics

LoopProtection

Main

RegisterCommand

Rewrite

SimpAll

SimpCongrTheorems

SimpTheorems

Simproc

Types

Try (file)

Collect

Acyclic

Apply

Assert

Assumption

AuxLemma

Backtrack

Cases

CasesOnStuckLHS

Cleanup

Clear

Congr

Constructor

Contradiction

Delta

ElimInfo

ExposeNames

Ext

FVarSubst

FunInd

FunIndCollect

FunIndInfo

Generalize

IndependentOf

Induction

Injection

Intro

Lets

LibrarySearch

NormCast

Refl

Rename

Repeat

Replace

Revert

Rewrite

Rewrites

Rfl

SolveByElim

Split

SplitIf

Subst

Symm

TryThis

Unfold

UnifyEq

Util

ACLt

AbstractMVars

AbstractNestedProofs

AppBuilder

Basic

BinderNameHint

Canonicalizer

CasesInfo

Check

CheckTactic

Closure

Coe

CoeAttr

CollectFVars

CollectMVars

CompletionName

CongrTheorems

CtorIdxHInj

CtorRecognizer

DecLevel

Diagnostics

Eqns

Eval

ExprDefEq

ExprLens

ExprTraverse

ForEachExpr

FunInfo

GeneralizeTelescope

GeneralizeVars

GetUnfoldableConst

HasAssignableMVar

HasNotBit

HaveTelescope

Hint

IndPredBelow

Inductive

InferType

Injective

Instances

IntInstTesters

Iterator

KAbstract

KExprMap

LazyDiscrTree

LetToHave

LevelDefEq

LitValues

MatchUtil

MethodSpecs

MkIffOfInductiveProp

MonadSimp

NatInstTesters

NatTable

Native

Offset

Order

PPBinder

PPGoal

PProdN

ProdN

RecExt

RecursorInfo

Reduce

ReduceEval

SameCtorUtils

SizeOf

Sorry

SplitSparseCasesOn

StringLitProof

Structure

SynthInstance

Transform

TransparencyMode

TryThis

UnificationHint

WHNF

WrapInstance

Parser (file)

Module (file)

Syntax

Tactic (file)

Doc

Term (file)

Basic

Doc

Attr

Basic

Command

Do

Extension

Extra

Level

StrInterpolation

Syntax

Types

ParserCompiler (file)

Attribute

PostprocessTraces (file)

Basic

PostprocessTracesCommand

Postprocessors

StoredTraces

PrettyPrinter (file)

Delaborator (file)

Attributes

Basic

Builtins

DeclWithSig

FieldNotation

Metavariable

Options

SubExpr

TopDownAnalyze

Basic

Formatter

Parenthesizer

Server (file)

CodeActions (file)

Attr

Basic

Provider

UnknownIdentifier

Completion (file)

CompletionCollectors

CompletionInfoSelection

CompletionItemCompression

CompletionResolution

CompletionUtils

EligibleHeaderDecls

ImportCompletion

SyntheticCompletion

FileWorker (file)

ExampleHover

InlayHints

RequestHandling

SemanticHighlighting

SetupFile

SignatureHelp

Utils

WidgetRequests

Rpc (file)

Basic

Deriving

RequestHandling

Test (file)

Cancel

Refs

Runner

AsyncList

FileSource

GoTo

InfoUtils

Logging

ProtocolOverview

References

RequestCancellation

Requests

ServerTask

Snapshots

Utils

Watchdog

Util (file)

CollectAxioms

CollectFVars

CollectLevelMVars

CollectLevelParams

CollectLooseBVars

CollectMVars

Diff

FVarSubset

FindExpr

FindLevelMVar

FindMVar

FoldConsts

ForEachExpr

ForEachExprWhere

HasConstCache

Heartbeats

InstantiateLevelParams

LakePath

LeanOptions

MonadBacktrack

MonadCache

NumApps

NumObjs

OccursCheck

PPExt

ParamMinimizer

Path

Profile

Profiler

ProfilerServer

PtrSet

RecDepth

Recognizers

ReplaceExpr

ReplaceLevel

Reprove

SCC

SafeExponentiation

ShareCommon

Sorry

SortExprs

TestExtern

Trace

UnusedBinders

Widget (file)

Basic

Commands

Diff

InteractiveCode

InteractiveDiagnostic

InteractiveGoal

TaggedText

Types

UserWidget

AddDecl

Attributes

AutoDecl

AuxRecursor

BuiltinDocAttr

Class

CompactedRegion

CoreM

Declaration

DeclarationRange

DefEqAttrib

DeprecatedModule

EnvExtension

Environment

ErrorExplanation

Exception

Expr

ExtraModUses

HeadIndex

Hygiene

IdentifierSuggestion

ImportingFlag

InternalExceptionId

KeyedDeclsAttribute

LabelAttribute

Level

LoadDynlib

LocalContext

Log

Message

MetavarContext

Modifiers

MonadEnv

Namespace

OriginalConstKind

PrivateName

ProjFns

ReducibilityAttrs

Replay

ReservedNameAction

ResolveName

Runtime

ScopedEnvExtension

Setup

Shell

Structure

SubExpr

Syntax

ToExpr

ToLevel

LeanSearchClient (file)

Basic

LoogleSyntax

Syntax

Mathlib

Algebra

Algebra

Spectrum

Basic

Pi

Quasispectrum

Subalgebra

Basic

Directed

IsSimpleOrder

Lattice

Operations

Pointwise

Prod

Tower

Basic

Bilinear

Defs

Equiv

Hom

IsSimpleRing

NonUnitalHom

NonUnitalSubalgebra

Operations

Opposite

Pi

Prod

Rat

RestrictScalars

StrictPositivity

Tower

TransferInstance

Unitization

ZMod

BigOperators

Finsupp

Basic

Fin

Group

Finset

Basic

Defs

Gaps

Indicator

Lemmas

Pi

Piecewise

Powerset

Preimage

Sigma

List

Basic

Defs

Lemmas

Multiset

Basic

Defs

GroupWithZero

Action

Finset

Ring

Finset

List

Multiset

Nat

Associated

Balance

Expect

Field

Fin

Finprod

Intervals

Module

NatAntidiagonal

Option

Pi

RingEquiv

WithTop

Category

Grp

Basic

ForgetCorepresentable

Limits

Preadditive

MonCat

Basic

ForgetCorepresentable

Limits

Ring

Adjunctions

Basic

Colimits

Constructions

Instances

Limits

Central

Basic

Defs

CharP

Algebra

Basic

CharAndCard

Defs

Frobenius

IntermediateField

Invertible

Lemmas

Reduced

Two

CharZero

AddMonoidHom

Defs

Infinite

Quotient

Colimit

DirectLimit

Finiteness

Module

TensorProduct

DirectSum

Algebra

Basic

Decomposition

Finsupp

Internal

Module

Ring

Divisibility

Basic

Hom

Units

EuclideanDomain

Basic

Defs

Field

Int

Exact

Basic

Field

Subfield

Basic

Defs

Basic

Defs

Equiv

GeomSum

IsField

NegOnePow

Opposite

Periodic

Rat

TransferInstance

ZMod

FiniteSupport

Basic

Defs

FreeAbelianGroup

Finsupp

FreeMonoid

Basic

UniqueProds

GCDMonoid

Basic

Finset

FinsetLemmas

IntegrallyClosed

Multiset

Nat

Group

Action

Pointwise

Set

Basic

Basic

Defs

End

Faithful

Hom

Opposite

Pi

Pretransitive

Prod

TransferInstance

TypeTags

Units

Commute

Basic

Defs

Hom

Units

Equiv

Basic

Defs

Opposite

TypeTags

Fin

Basic

Tuple

Hom

Basic

CompTypeclasses

Defs

End

Instances

Int

Defs

Even

Units

Invertible

Basic

Defs

Irreducible

Defs

Lemmas

Nat

Defs

Even

Hom

Units

Pi

Basic

Lemmas

Torsion

Units

Pointwise

Finset

Basic

Scalar

Set

Basic

BigOperators

Card

Finite

Lattice

ListOfFn

Scalar

Semiconj

Basic

Defs

Units

Subgroup

ZPowers

Basic

Lemmas

Actions

Basic

Defs

Finite

Finsupp

Ker

Lattice

Map

MulOpposite

MulOppositeLemmas

Order

Pointwise

Submonoid

Basic

BigOperators

Defs

DistribMulAction

Finite

Membership

MulAction

MulOpposite

Operations

Pointwise

Support

Units

Subsemigroup

Basic

Defs

Membership

MulOpposite

Operations

TypeTags

Basic

Finite

Hom

Pointwise

UniqueProds

Basic

Units

Basic

Defs

Equiv

Hom

Opposite

WithOne

Defs

Map

AddChar

Basic

Center

Commutator

Conj

Defs

DivInvMonoid

Embedding

End

Even

EvenFunction

Finsupp

FunLike

Graph

Idempotent

Indicator

InjSurj

IsApply

IsCommutative

ModEq

Monoid

NatPowAssoc

Opposite

PUnit

Prod

SelfInv

Semigroup

Shrink

Support

Torsion

TransferInstance

ULift

GroupWithZero

Action

Pointwise

Set

Basic

Defs

End

Hom

Opposite

Pi

Prod

Regular

TransferInstance

Units

Pointwise

Set

Basic

Submonoid

Instances

Pointwise

Primal

Units

Basic

Equiv

Fintype

Lemmas

Associated

Basic

Center

Commute

Defs

Divisibility

Equiv

Hom

Idempotent

Indicator

InjSurj

Invertible

Nat

NeZero

NonZeroDivisors

Opposite

Pi

Prod

Range

Regular

Semiconj

Subgroup

ULift

WithZero

Module

Congruence

Defs

Equiv

Basic

Defs

Opposite

LinearMap

Basic

Defs

DivisionRing

End

Prod

Star

LocalizedModule

AtPrime

Basic

IsLocalization

Submodule

Submodule

Basic

Bilinear

Defs

EqLocus

Equiv

Finsupp

Invariant

IterateMapComap

Ker

Lattice

LinearMap

Map

Pointwise

Range

RestrictScalars

Torsion

Basic

Field

Free

Pi

Basic

BigOperators

Defs

End

FunLike

Hom

MinimalAxioms

NatInt

Opposite

PUnit

Pi

Prod

Projective

Rat

RingHom

Shrink

SpanRank

TransferInstance

ULift

ZMod

MonoidAlgebra

Basic

Defs

Degree

Division

Lift

MapDomain

Module

NoZeroDivisors

Opposite

Support

MvPolynomial

Basic

Coeff

CommRing

Degrees

Derivation

Equiv

Eval

Expand

Funext

Monad

Nilpotent

PDeriv

Polynomial

Rename

SchwartzZippel

Supported

Variables

NoZeroSMulDivisors

Basic

Defs

Notation (file)

Pi

Basic

Defs

Bracket

Defs

FiniteSupport

Indicator

Lemmas

Prod

Support

Order

AbsoluteValue

Basic

Antidiag

Finsupp

Pi

Prod

Archimedean

Real

Basic

Basic

Defs

BigOperators

Group

Finset

List

LocallyFinite

Multiset

GroupWithZero

Finset

List

Multiset

Ring

Finset

List

Multiset

Expect

CauSeq

Basic

BigOperators

Completion

Field

Basic

Canonical

GeomSum

Power

Rat

Floor

Defs

Div

Ring

Semifield

Semiring

Group

Action (file)

Synonym

Pointwise

Bounds

CompleteLattice

Interval

Unbundled

Abs

Basic

Int

Abs

Basic

Cyclic

Defs

DenselyOrdered

Finset

Indicator

Int

Lattice

MinMax

Multiset

Nat

Opposite

OrderIso

PiLex

PosPart

Synonym

Units

GroupWithZero

Action

Synonym

Basic

Canonical

Defs

Finset

OrderIso

Range

Submonoid

Synonym

WithZero

Hom

Basic

GroupNorm

Monoid

MonoidWithZero

Ring

RingNorm

TypeTags

Units

Interval

Finset

Basic

SuccPred

Set

Group

Instances

Monoid

Module

Basic

Defs

Field

Pointwise

PositiveLinearMap

Rat

Synonym

Monoid

Canonical

Basic

Defs

Unbundled

Basic

Defs

ExistsOfLE

MinMax

OrderDual

Pow

TypeTags

WithTop

Basic

Defs

Multiset

NatCast

OrderDual

Prod

Submonoid

TypeTags

Units

WithTop

Nonneg

Basic

Field

Floor

Lattice

Module

Ring

Positive

Ring

Ring

Unbundled

Basic

Rat

Abs

Basic

Canonical

Cast

Defs

Finset

GeomSum

Idempotent

InjSurj

Int

Interval

IsNonarchimedean

NNRat

Nat

Pow

Rat

Star

Synonym

WithTop

Star

Basic

Prod

Real

Sub

Unbundled

Basic

Basic

Defs

WithTop

SuccPred (file)

PartialSups

WithBot

AddGroupWithTop

AddTorsor

Algebra

Chebyshev

Invertible

IsBotOne

Kleene

Monovary

Pi

Rearrangement

Round

ToIntervalMod

ZeroLEOne

Polynomial

Degree

Defs

Domain

IsMonicOfDegree

Lemmas

Monomial

Operations

SmallDegree

Support

TrailingDegree

Units

Eval

Algebra

Coeff

Defs

Degree

SMul

Subring

Module

AEval

Basic

AlgebraMap

Basic

BigOperators

CancelLeads

Coeff

CoeffMem

Derivative

Div

EraseLead

Expand

FieldDivision

GroupRingAction

HasseDeriv

Identities

Inductions

Laurent

Lifts

Monic

Monomial

OfFn

Reverse

RingDivision

Roots

Smeval

SpecificDegree

Splits

Taylor

Prime

Defs

Lemmas

Regular

Basic

Defs

Opposite

Pow

SMul

Ring

Action

Pointwise

Set

Basic

ConjAct

End

Field

Group

Invariant

Rat

Submonoid

Subobjects

Divisibility

Basic

Hom

Defs

InjSurj

Int

Defs

Field

Parity

Units

Submonoid

Basic

Pointwise

Subring

Basic

Defs

Pointwise

Units

Subsemiring

Basic

Defs

Pointwise

AddAut

Associated

Associator

Aut

Basic

BooleanRing

Center

Centralizer

CharZero

Commute

CompTypeclasses

Defs

Equiv

Fin

FunLike

GeomSum

GrindInstances

Idempotent

InjSurj

Invertible

Nat

NegOnePow

NonZeroDivisors

Opposite

PUnit

Parity

Periodic

Pi

Prod

Rat

Regular

Semiconj

Shrink

Torsion

TransferInstance

ULift

Units

Squarefree

Basic

Star

Basic

BigOperators

Center

Module

MonoidHom

NonUnitalSubalgebra

Pi

Pointwise

Prod

Rat

SelfAdjoint

StarAlgHom

StarProjection

StarRingHom

Subalgebra

TensorProduct

Unitary

UnitaryStarAlgAut

Torsor

Basic

Defs

TrivSqZeroExt

Basic

DualNumber

FreeAlgebra

GradedMonoid

GradedMulAction

IsPrimePow

NeZero

Opposites

QuadraticDiscriminant

Quotient

Analysis

Analytic

Basic

CPolynomial

CPolynomialDef

ChangeOrigin

Composition

Constructions

ConvergenceRadius

Inverse

IsolatedZeros

Linear

OfScalars

Polynomial

Uniqueness

Within

Asymptotics

Arith

AsymptoticEquivalent

Basic

Defs

Lemmas

Prod

Ring

SpecificAsymptotics

TVS

Theta

BoxIntegral

Box

Basic

SubboxInduction

Partition

Additive

Basic

Filter

Measure

Split

SubboxInduction

Tagged

Basic

DivergenceTheorem

Integrability

CStarAlgebra

ContinuousFunctionalCalculus

Commute

Continuity

Instances

Isometric

NonUnital

Pi

Restrict

Unique

Unital

Basic

Classes

Matrix

Unitization

Calculus

ContDiff

Basic

Comp

Defs

Deriv

FTaylorSeries

FaaDiBruno

Operations

RCLike

WithLp

Deriv

Add

AffineMap

Basic

Comp

CompMul

Inv

Inverse

Linear

MeanValue

Mul

Polynomial

Pow

Prod

Shift

Slope

Support

ZPow

FDeriv

Add

Affine

Analytic

Basic

Bilinear

Comp

CompCLM

Congr

Const

Defs

Equiv

Extend

Linear

Measurable

Mul

OfCompLeft

Pow

Prod

RestrictScalars

WithLp

InverseFunctionTheorem

ApproximatesLinearOn

Deriv

FDeriv

IteratedDeriv

Defs

Lemmas

LocalExtr

Basic

Rolle

TangentCone

Basic

Defs

DimOne

Prod

Real

DSlope

DiffContOnCl

FormalMultilinearSeries

LagrangeMultipliers

LogDeriv

MeanValue

Monotone

ParametricIntegral

ParametricIntervalIntegral

Taylor

Complex

Polynomial

Basic

Arg

Asymptotics

Basic

Cardinality

CauchyIntegral

Circle

Convex

Exponential

ExponentialBounds

Liouville

Norm

Order

ReImTopology

RealDeriv

Spectrum

Trigonometric

Convex

Cone

Extension

SpecificFunctions

Basic

Deriv

Pow

Basic

Birkhoff

Combination

Deriv

DoublyStochasticMatrix

EGauge

Extreme

Function

Gauge

Hull

Jensen

Mul

PathConnected

Segment

Slope

Star

StdSimplex

Strict

StrictConvexSpace

Topology

Uniform

Fourier

BoundedContinuousFunctionChar

FourierTransform

Notation

InnerProductSpace

Projection

Basic

FiniteDimensional

Minimal

Reflection

Submodule

Adjoint

Basic

Calculus

Continuous

Convex

Defs

Dual

GramMatrix

GramSchmidtOrtho

LinearMap

Orientation

Orthogonal

Orthonormal

PiL2

Positive

ProdL2

Rayleigh

Spectrum

Subspace

Symmetric

LocallyConvex

BalancedCoreHull

Basic

Bounded

ContinuousOfBounded

HahnBanach

SeparatingDual

Separation

WeakDual

WithSeminorms

Matrix

Hermitian

HermitianFunctionalCalculus

MeasurableSpace

Normed

Order

PosDef

Spectrum

Normed

Affine

AddTorsor

Isometry

Algebra

Exponential

Spectrum

Unitization

UnitizationL1

Field

Basic

Lemmas

UnitBall

Group

AddCircle

AddTorsor

BallSphere

Basic

Bounded

Completion

Constructions

Continuity

Defs

FunctionSeries

Hom

Indicator

InfiniteSum

Int

Lemmas

NullSubmodule

Pointwise

Quotient

RadialFunction

Rat

Real

Seminorm

Subgroup

Submodule

Uniform

Lp

Matrix

MeasurableSpace

PiLp

ProdLp

WithLp

Module

Alternating

Basic

Ball

Homeomorph

Pointwise

Multilinear

Basic

Curry

RCLike

Basic

Extend

Real

Seminorm

Basic

Norm

Basic

Completion

Convex

FiniteDimension

HahnBanach

Ray

RieszLemma

Span

Operator

Compact

Basic

FiniteDimension

FredholmAlternative

Asymptotics

Banach

Basic

Bilinear

BoundedLinearMaps

CompleteCodomain

ContinuousLinearMap

Extend

LinearIsometry

Mul

NNNorm

NormedSpace

Order

Lattice

Ring

Basic

Finite

InfiniteSum

Lemmas

Units

MulAction

RCLike

Basic

BoundedContinuous

Extend

Lemmas

Sqrt

Real

Pi

Bounds

Wallis

Cardinality

Spectrum

Sqrt

SpecialFunctions

Complex

Analytic

Arg

Circle

CircleAddChar

CircleMap

Log

LogBounds

LogDeriv

ContinuousFunctionalCalculus

PosPart

Basic

Rpow

Basic

Isometric

Measurable

Abs

Gamma

Basic

Gaussian

FourierTransform

GaussianIntegral

Integrability

Basic

Integrals

Basic

Log

Base

Basic

Deriv

ENNRealLog

InvLog

NegMulLog

Pow

Asymptotics

Complex

Continuity

Deriv

NNReal

NthRootLemmas

Real

Trigonometric

Angle

Arctan

ArctanDeriv

Basic

Bounds

Complex

ComplexDeriv

Deriv

Inverse

InverseDeriv

Sinc

Bernstein

BinaryEntropy

Exp

ExpDeriv

Exponential

ImproperIntegrals

JapaneseBracket

MulExpNegMulSq

MulExpNegMulSqIntegral

NonIntegrable

PolarCoord

Sqrt

Stirling

SpecificLimits

ArithmeticGeometric

Basic

Normed

RCLike

BoundedVariation

LConvolution

MeanInequalities

MeanInequalitiesPow

Oscillation

Basic

Complex

Basic

BigOperators

Countable

Basic

Defs

Small

ENNReal

Action

Basic

BigOperators

Holder

Inv

Lemmas

Operations

Real

Finite

Defs

Prod

Set

Sigma

Sum

FunLike

Basic

Embedding

Equiv

IsEmpty

Basic

Defs

Logic

Basic

Lemmas

NNReal

Basic

Defs

Star

Nontrivial

Basic

Defs

Real

Basic

ConjExponents

ENatENNReal

Pointwise

Star

Rel (file)

Cover

Separated

SetLike

Basic

Sign

Basic

Defs

Denumerable

ExistsUnique

Nonempty

Opposite

PEquiv

SProd

Unique

UnivLE

CategoryTheory

Adjunction

Basic

FullyFaithful

Limits

Mates

Bicategory

Functor

Lax

Oplax

Prelax

Pseudofunctor

Strict

Basic

Basic

Free

Category

Cat (file)

AsSmall

Basic

Init

Preorder

RelCat

ULift

Comma

Over

Basic

Pullback

StructuredArrow

Basic

Arrow

Basic

ConcreteCategory

Basic

Bundled

Elementwise

Forget

Notation

ReflectsIso

Discrete

Basic

EffectiveEpi

Basic

Filtered

Basic

Connected

FinCategory

AsType

Basic

Functor

ReflectsIso

Basic

Basic

Category

Const

Currying

EpiMono

FullyFaithful

Hom

Trifunctor

TwoSquare

LiftingProperties

Adjunction

Basic

Limits

ConcreteCategory

Basic

Constructions

BinaryProducts

FunctorCategory

Basic

Preserves

Shapes

Pullbacks

Terminal

Zero

Basic

Limits

Ulift

Shapes

BinaryProducts

BinaryFan

BinaryProducts

WalkingPair

Opposites

Equalizers

Pullbacks

Pullback

IsPullback

Basic

Defs

Assoc

Cospan

HasPullback

Iso

Mono

Pasting

PullbackCone

Diagonal

Equalizers

FiniteLimits

Grothendieck

Images

IsTerminal

KernelPair

Kernels

Products

RegularMono

StrictInitial

StrongEpi

Terminal

WidePullbacks

ZeroMorphisms

ZeroObjects

Types

ColimitType

Colimits

Filtered

Images

Limits

Products

Cones

Connected

Creates

Final

HasLimits

IsLimit

Opposites

Yoneda

Monad

Algebra

Basic

Products

Monoidal

Free

Basic

Category

Functor

MorphismProperty

Basic

Composition

Factorization

Limits

ObjectProperty

Basic

ClosedUnderIsomorphisms

CompleteLattice

Equivalence

FullSubcategory

Opposite

Small

Pi

Basic

Preadditive

Basic

Products

Basic

Unitor

Types

Basic

Balanced

CofilteredSystem

CommSq

Elements

Elementwise

Endomorphism

EpiMono

EqToHom

Equivalence

EssentialImage

EssentiallySmall

Grothendieck

Groupoid

HomCongr

InducedCategory

IsConnected

Iso

IsomorphismClasses

NatIso

NatTrans

Opposites

PEmpty

PUnit

Retract

ShrinkYoneda

Skeletal

Thin

Whiskering

Yoneda

Combinatorics

Digraph

Basic

Enumerative

Partition

Basic

Composition

DoubleCounting

InclusionExclusion

Stirling

Hall

Basic

Finite

Matroid

Minor

Restrict

Rank

Cardinal

ENat

Finite

Basic

Circuit

Closure

Constructions

Dual

IndepAxioms

Init

Loop

Map

Quiver

Basic

Path

Prefunctor

Push

Symmetric

SetFamily

Compression

Down

Shatter

SimpleGraph

Coloring

Vertex

Connectivity

Connected

EdgeConnectivity

Finite

Subgraph

Walk

Basic

Chord

Counting

Decomp

Maps

Operations

Subwalks

Traversal

Acyclic

Basic

Bipartite

Clique

Copy

CycleGraph

Dart

DegreeSum

DeleteEdges

Finite

Hasse

Init

Maps

Metric

Operations

Paths

Prod

Subgraph

Sum

Colex

Pigeonhole

Computability

TuringMachine

PostTuringMachine

StackTuringMachine

Tape

DFA

Language

NFA

RegularExpressions

StateTransition

Control

Monad

Basic

Cont

Writer

Traversable

Basic

Lemmas

Applicative

Basic

Bifunctor

Combinators

EquivFunctor

Functor

Lawful

ULift

ULiftable

Data

Bool

AllAny

Basic

Set

DFinsupp

BigOperators

Defs

Ext

Lex

Module

NeLocus

Order

Sigma

Small

Submonoid

WellFounded

ENat

Basic

Defs

Lattice

Monoid

Pow

EReal

Basic

Inv

Operations

Fin

Tuple

Basic

Finset

NatAntidiagonal

Reflection

Sort

Take

Basic

Embedding

Rev

SuccPred

VecNotation

Finite

Perm

Finset

Lattice

Basic

Fold

Lemmas

Prod

Union

Attach

Attr

Basic

BooleanAlgebra

Card

Dedup

Defs

Density

Disjoint

Empty

Erase

Filter

Fin

Fold

Image

Insert

Max

MulAntidiagonal

NAry

NatAntidiagonal

NoncommProd

Option

Order

Pairwise

Pi

Piecewise

Powerset

Preimage

Prod

Range

SDiff

SMulAntidiagonal

Sigma

Slice

Sort

Sum

Sym

SymmDiff

Union

Update

Finsupp

Antidiagonal

Basic

Defs

Ext

Fin

Fintype

Indicator

Lex

Multiset

Option

Order

PWO

SMul

SMulWithZero

Single

ToDFinsupp

Weight

WellFounded

Fintype

Basic

BigOperators

Card

CardEmbedding

Defs

EquivFin

Fin

Inv

Lattice

List

OfMap

Option

Order

Parity

Perm

Pi

Pigeonhole

Powerset

Prod

Quotient

Sets

Sigma

Sort

Sum

Vector

FunLike

Fintype

Int

Cast

Basic

Defs

Field

Lemmas

Pi

Prod

Order

Basic

Units

Basic

CharZero

DivMod

GCD

Init

Interval

Log

ModEq

NatAbs

Notation

Range

Sqrt

WithZero

List

Perm

Basic

Lattice

Subperm

Basic

Chain

Count

Cycle

Dedup

Defs

Duplicate

Enum

FinRange

Find

Flatten

Forall2

GetD

Induction

Infix

InsertIdx

Iterate

Lattice

Lex

MinMax

ModifyLast

Monad

NatAntidiagonal

Nodup

NodupEquivFin

OfFn

OffDiag

Pairwise

Permutation

Pi

Prime

ProdSigma

Range

Rotate

Sort

Sublists

Sym

TFAE

TakeDrop

ToFinsupp

Zip

Matrix

Basic

Basis

Block

ColumnRowPartitioned

Composition

Diagonal

Mul

PEquiv

Reflection

Multiset

AddSub

Antidiagonal

Basic

Bind

Count

Dedup

Defs

Filter

Find

FinsetOps

Fintype

Fold

Lattice

MapFold

NatAntidiagonal

Pi

Powerset

Range

Replicate

Sections

Sort

Sum

Sym

UnionInter

ZeroCons

NNRat

Defs

Nat

Cast

Order

Basic

Field

Ring

Basic

Commute

Defs

Field

NeZero

Prod

WithTop

Choose

Basic

Bounds

Cast

Central

Dvd

Factorization

Multinomial

Sum

Vandermonde

Digits

Defs

Lemmas

Factorial

Basic

BigOperators

Cast

DoubleFactorial

SuperFactorial

Factorization

Basic

Defs

Induction

LCM

PrimePow

Fib

Basic

GCD

Basic

BigOperators

NthRoot

Defs

Order

Lemmas

Prime

Basic

Defs

Factorial

Infinite

Int

Nth

Pow

Basic

BinaryRec

BitIndices

Bits

Bitwise

Count

Dist

DvdSequence

Factors

Find

Init

Log

MaxPowDiv

ModEq

Multiplicity

Notation

Nth

PadicValNat

Pairing

Periodic

PrimeFin

Set

Size

Sqrt

Squarefree

Totient

WithBot

Option

Basic

Defs

NAry

Ordering

Basic

PNat

Basic

Defs

Equiv

Notation

Prime

Prod

Basic

PProd

TProd

Rat

Cast

CharZero

Defs

Lemmas

Order

BigOperators

Defs

Encodable

Floor

Init

Lemmas

Sqrt

Seq

Basic

Computation

Defs

Set

Card (file)

Arithmetic

Finite

Basic

Lattice

Lemmas

Powerset

Range

Lattice

Bounded

Disjoint

Image

Indexed

Order

Pairwise

Basic

Lattice

List

Basic

BoolIndicator

BooleanAlgebra

CoeSort

Constructions

Countable

Defs

Disjoint

Function

Functor

Image

Inclusion

Insert

List

MemPartition

Monotone

MulAntidiagonal

NAry

Notation

Operations

Order

Piecewise

Prod

Restrict

SMulAntidiagonal

Semiring

Sigma

Subset

Subsingleton

SymmDiff

UnionLift

SetLike

Fintype

Sigma

Basic

Stream

Defs

Init

String

Defs

Sum

Basic

Sym

Sym2 (file)

Init

Basic

Card

Tree

Basic

Vector

Basic

Defs

W

Basic

Cardinal

ZMod

Aut

Basic

Defs

IntUnitsPower

QuotientGroup

QuotientRing

Units

ValMinAbs

Bundle

Dyadic

FinEnum

Ineq

PFun

Part

Quot

Subtype

ULift

Dynamics

Ergodic

MeasurePreserving

FixedPoints

Basic

Defs

Topology

PeriodicPts

Defs

Lemmas

Minimal

FieldTheory

Finite

Basic

GaloisField

Polynomial

Trace

Galois

Abelian

Basic

GaloisClosure

Infinite

Notation

IntermediateField

Adjoin

Algebra

Basic

Defs

Algebraic

Basic

IsAlgClosed

AlgebraicClosure

Basic

Spectrum

Minpoly

Basic

Field

Finite

IsIntegrallyClosed

MinpolyDiv

Normal

Basic

Closure

Defs

PurelyInseparable

Basic

RatFunc

AsPolynomial

Basic

Defs

SplittingField

Construction

IsSplittingField

AlgebraicClosure

ChevalleyWarning

Extension

Finiteness

Fixed

IsSepClosed

KrullTopology

KummerExtension

KummerPolynomial

Perfect

PolynomialGaloisGroup

PrimitiveElement

Separable

SeparableClosure

SeparableDegree

Tower

Geometry

Convex

Cone

Basic

Pointed

ConvexSpace

AffineMap

Barycenter

CompactSpaceStdSimplex

Defs

Module

ModuleTopology

PathConnectedSpaceStdSimplex

Prod

Topology

Set

Star

GroupTheory

Abelianization

Defs

Commutator

Basic

Congruence

Basic

BigOperators

Defs

Hom

Opposite

Coset

Basic

Card

Defs

FreeGroup

Basic

GroupAction

DomAct

Basic

SubMulAction (file)

Pointwise

Basic

ConjAct

Defs

FixedPoints

FixingSubgroup

Hom

IterateAct

Pointwise

Quotient

Ring

MonoidLocalization

Away

Basic

Divisibility

Maps

MonoidWithZero

OreLocalization

Basic

OreSet

Perm

Cycle

Basic

Factors

Type

Basic

Closure

Fin

Finite

List

Option

Sign

Support

ViaEmbedding

QuotientGroup

Basic

Defs

Finite

ModEq

SpecificGroups

Cyclic (file)

Basic

Subgroup

Center

Centralizer

Simple

Submonoid

Center

Centralizer

Subsemigroup

Center

Centralizer

Lemmas

Archimedean

Complement

DedekindFinite

Divisible

Exponent

Finiteness

FreeAbelianGroup

Index

NoncommPiCoprod

OrderOfElement

PGroup

Rank

Solvable

Sylow

Torsion

InformationTheory

Hamming

Lean

Elab

Tactic

Basic

Meta

InfoTree

Term

Expr

Basic

ExtraRecognizers

Rat

MessageData

Trace

Meta (file)

RefinedDiscrTree (file)

Basic

Encode

Initialize

Lookup

Tactic

Rewrite

Basic

CongrTheorems

KAbstractPositions

Simp

PrettyPrinter

Delaborator

ContextInfo

Environment

FoldEnvironment

GoalsLocation

Linter

Name

LinearAlgebra

AffineSpace

AffineSubspace

Basic

Defs

Simplex

Basic

AffineEquiv

AffineMap

Basis

Centroid

Combination

Defs

Independent

Midpoint

Ordered

Pointwise

Restrict

Slope

Alternating

Basic

Basis

Basic

Bilinear

Cardinality

Defs

Fin

Prod

SMul

Submodule

VectorSpace

BilinearForm

Basic

DualLattice

Hom

Orthogonal

Properties

Charpoly

BaseChange

Basic

ToMatrix

Complex

FiniteDimensional

Module

Dimension

Basic

Constructions

DivisionRing

ErdosKaplansky

Finite

Finrank

Free

FreeAndStrongRankCondition

LinearMap

Localization

OrzechProperty

RankNullity

StrongRankCondition

Subsingleton

DirectSum

Finsupp

TensorProduct

Dual

Basis

Defs

Lemmas

Eigenspace

Basic

Charpoly

ContinuousLinearMap

Matrix

Minpoly

Zero

FiniteDimensional

Basic

Defs

Lemmas

Finsupp

Defs

LSum

LinearCombination

Pi

Span

SumProd

Supported

VectorSpace

FreeModule

Finite

Basic

Matrix

Basic

PID

StrongRankCondition

GeneralLinearGroup

AlgEquiv

Basic

LinearIndependent

Algebra

Basic

Defs

Lemmas

Matrix

Charpoly

Basic

Coeff

Eigs

LinearMap

Minpoly

Determinant

Bird

Correctness

Defs

Basic

Echelon

Basic

Decomposition

Pivot

GeneralLinearGroup

Defs

Action

Adjugate

Basis

BilinearForm

Block

ConjTranspose

Defs

Diagonal

DotProduct

Dual

Hadamard

Hermitian

Ideal

InvariantBasisNumber

Invertible

Kronecker

MvPolynomial

Nondegenerate

NonsingularInverse

Notation

Permutation

Polynomial

PosDef

Rank

Reindex

RowCol

SchurComplement

SemiringInverse

SesquilinearForm

SpecialLinearGroup

StdBasis

Stochastic

Symmetric

ToLin

ToLinearEquiv

Trace

Transvection

Unique

Vec

ZPow

Multilinear

Basic

Basis

Curry

DFinsupp

Finsupp

Projectivization

Basic

Cardinality

QuadraticForm

Basic

Quotient

Basic

Card

Defs

SModEq

Basic

SesquilinearForm

Basic

Orthogonal

Span

Basic

Defs

TensorProduct

Associator

Basic

Basis

Defs

DirectLimit

Finiteness

Lift

Map

Quotient

RightExactness

Tower

BilinearMap

Contraction

DFinsupp

Determinant

InvariantBasisNumber

Isomorphisms

Lagrange

LinearPMap

Orientation

Pi

Prod

Projection

Ray

StdBasis

Trace

UnitaryGroup

Vandermonde

Logic

Embedding

Basic

Set

Encodable

Basic

Lattice

Pi

Equiv

Fin

Basic

Rotate

Basic

Bool

Defs

Embedding

Finset

Fintype

Functor

List

Multiset

Nat

Option

PartialEquiv

Prod

Set

Sigma

Sum

Function

Basic

CompTypeclasses

Conjugate

Defs

DependsOn

Iterate

ULift

Small

Basic

Defs

List

Set

OpClass

Pairwise

Relation

Relator

MeasureTheory

Constructions

BorelSpace

Basic

Complex

ContinuousLinearMap

Metric

Metrizable

Order

Real

Polish

Basic

StronglyMeasurable

Pi

Covering

Besicovitch

BesicovitchVectorSpace

DensityTheorem

Differentiation

OneDim

Vitali

VitaliFamily

Function

ConditionalExpectation

AEMeasurable

Basic

CondexpL1

CondexpL2

Unique

L1Space

AEEqFun

HasFiniteIntegral

Integrable

LpSeminorm

Basic

ChebyshevMarkov

CompareExp

Defs

Indicator

Monotonicity

Prod

SMul

TriangleInequality

Trim

LpSpace

Basic

Complete

CompleteOfCompleteLp

ContinuousFunctions

Indicator

InfiniteSum

SpecialFunctions

Basic

StronglyMeasurable

AEStronglyMeasurable

Basic

ENNReal

Inner

Lemmas

Lp

AEEqFun

AEEqOfIntegral

AEEqOfLIntegral

AEMeasurableOrder

AEMeasurableSequence

AbsolutelyContinuous

ConvergenceInMeasure

Egorov

EssSup

Floor

Jacobian

JacobianOneDim

L2Space

LocallyIntegrable

LpOrder

SimpleFunc

SimpleFuncDense

SimpleFuncDenseLp

UniformIntegrable

Group

Action

Arithmetic

Convolution

Defs

FundamentalDomain

Integral

IntegralConvolution

LIntegral

MeasurableEquiv

Measure

Pointwise

Prod

Integral

Bochner

Basic

ContinuousLinearMap

FundThmCalculus

L1

Set

SumMeasure

VitaliCaratheodory

IntervalIntegral

AbsolutelyContinuousFun

Basic

DerivIntegrable

FundThmCalculus

IntegrationByParts

LebesgueDifferentiationThm

Periodic

Slope

Lebesgue

Add

Basic

Countable

DominatedConvergence

Map

Markov

Norm

Sub

SetToL1

ChangeMeasure

DominatedConvergence

Function

L1

SimpleFunc

Asymptotics

Average

BoundedContinuousFunction

CircleIntegral

DivergenceTheorem

DominatedConvergence

ExpDecay

FinMeasAdditive

IntegrableOn

IntegralEqImproper

Layercake

Marginal

MeanInequalities

Pi

Prod

MeasurableSpace

Basic

Constructions

CountablyGenerated

Defs

Embedding

EventuallyMeasurable

Instances

MeasurablyGenerated

Pi

Prod

Measure

CharacteristicFunction

Basic

Decomposition

Exhaustion

Hahn

Lebesgue

RadonNikodym

Dirac

Basic

Def

Haar

Basic

InnerProductSpace

NormedSpace

OfBasis

Quotient

Unique

Lebesgue

Basic

Complex

EqHaar

Integral

Typeclasses

Finite

NullSingletonClass

Probability

SFinite

AEDisjoint

AEMeasurable

AbsolutelyContinuous

Basic

Comap

CompleteLattice

Content

Continuity

Count

Doubling

EverywherePos

Filter

FiniteMeasureExt

GiryMonad

HasOuterApproxClosed

Interval

Map

MeasureSpaceDef

Module

MutuallySingular

NullMeasurable

OpenPos

OuterMeasure

Prod

QuasiMeasurePreserving

Real

Regular

RegularityCompacts

Restrict

Stieltjes

Sub

Sum

Trim

WithDensity

Order

Lattice

OuterMeasure

AE

Basic

BorelCantelli

Caratheodory

Defs

Induced

OfFunction

Operations

SpecificCodomains

Pi

WithLp

PiSystem

Topology

NumberTheory

ArithmeticFunction

Defs

Misc

Moebius

VonMangoldt

Zeta

Cyclotomic

Basic

PrimitiveRoots

LegendreSymbol

QuadraticChar

Basic

GaussSum

AddCharacter

Basic

JacobiSymbol

QuadraticReciprocity

ZModChar

MulChar

Basic

Lemmas

NumberField

Basic

Padics

PadicVal

Basic

Defs

Real

Irrational

Zsqrtd

Basic

AbelSummation

Chebyshev

Divisors

GaussSum

PrimeCounting

Primorial

Order

Atoms (file)

Finite

BooleanAlgebra

Basic

Defs

Set

BoundedOrder

Basic

Lattice

Monotone

Bounds

Basic

Defs

Image

OrderIso

CompactlyGenerated

Basic

Intervals

CompleteLattice

Basic

Chain

Defs

Finset

Group

Lemmas

ConditionallyCompleteLattice

Basic

Defs

Finset

Group

Indexed

ConditionallyCompletePartialOrder

Basic

Defs

Indexed

Defs

Lattice

LinearOrder

PartialOrder

Prop

Unbundled

Filter

AtTopBot

Archimedean

Basic

BigOperators

CompleteLattice

CountablyGenerated

Defs

Disjoint

Field

Finite

Finset

Floor

Group

Map

ModEq

Monoid

Prod

Ring

Tendsto

Bases

Basic

Finite

Germ

Basic

OrderedMonoid

Ultrafilter

Basic

Defs

Basic

Cofinite

CountableInter

CountableSeparatingOn

CountablyGenerated

Curry

Defs

ENNReal

EventuallyConst

Extr

Finite

IndicatorFunction

Interval

IsBounded

Ker

Lift

Map

NAry

Pi

Pointwise

Prod

Ring

SmallSets

Subsingleton

Tendsto

TendstoCofinite

Fin

Basic

Tuple

GaloisConnection

Basic

Defs

Heyting

Basic

Boundary

Hom

Hom

Basic

Bounded

BoundedLattice

CompleteLattice

Lattice

Lex

Order

Set

WithTopBot

Int

ConditionallyCompleteOrder

LeastGreatest

Interval

Finset

Basic

Defs

Fin

Gaps

Nat

SuccPred

Set

Basic

Defs

Disjoint

Fin

Image

Infinite

LinearOrder

Monotone

OrdConnected

OrdConnectedComponent

OrderEmbedding

OrderIso

Pi

ProjIcc

SuccPred

UnorderedInterval

WithBotTop

Multiset

Lattice (file)

Nat

Monotone

Basic

Defs

Extension

Monovary

Partition

Finpartition

Preorder

Chain

Finite

Finsupp

Prod

Lex

Basic

RelIso

Basic

Set

Setoid

Basic

Partition

Sigma (file)

Lex

SuccPred

Archimedean

Basic

CompleteLinearOrder

ENat

Fin

InitialSeg

Int

IntervalSucc

Limit

LinearLocallyFinite

Nat

Relation

WithBot

Sum

Order

UpperLower

Basic

Closure

CompleteLattice

Fibration

Principal

Antichain

Antisymmetrization

Basic

BooleanSubalgebra

BourbakiWitt

Circular

Closure

Cofinal

Compare

CompleteBooleanAlgebra

CompleteLatticeIntervals

Copy

Cover

DirSupClosed

Directed

DirectedInverseSystem

Disjoint

Disjointed

FixedPoints

GameAdd

Ideal

InitialSeg

IsNormal

Iterate

JordanHolder

KrullDimension

LatticeIntervals

Lex

LiminfLimsup

Max

MinMax

Minimal

ModularLattice

Nat

Notation

OmegaCompletePartialOrder

OrdContinuous

OrderDual

OrderIsoNat

Part

PartialSups

PiLex

PropInstances

RelClasses

RelSeries

ScottContinuity

SetAccumulate

SetDissipate

SetNotation

Shrink

Sublattice

SupClosed

SupIndep

SymmDiff

TypeTags

ULift

WellFounded

WellFoundedSet

WellQuasiOrder

WithBot

Zorn

ZornAtoms

Probability

Distributions

Gaussian

HasGaussianLaw

Basic

Def

Independence

Basic

CharFun

Fernique

Multivariate

Real

Bernoulli

Fernique

Independence

Kernel

Indep

IndepFun

Basic

CharacteristicFunction

Integrable

Integration

Kernel

Composition

Comp

CompMap

CompNotation

CompProd

KernelLemmas

MapComap

MeasureComp

MeasureCompProd

ParallelComp

Prod

Basic

Defs

MeasurableLIntegral

Moments

Basic

ComplexMGF

Covariance

CovarianceBilin

CovarianceBilinDual

IntegrableExpMul

MGFAnalytic

Variance

ProbabilityMassFunction

Basic

Constructions

Monad

ConditionalProbability

Density

HasLaw

IdentDistrib

Notation

UniformOn

RingTheory

AdicCompletion

Basic

Adjoin

Polynomial

Basic

Transcendental

Basic

Dimension

FG

FGBaseChange

Field

PowerBasis

Singleton

Tower

Algebraic

Basic

Defs

Integral

MvPolynomial

AlgebraicIndependent

Adjoin

AlgebraicClosure

Basic

Defs

TranscendenceBasis

Transcendental

Artinian

Defs

Module

Congruence

Basic

Defs

Opposite

Coprime

Basic

Ideal

Lemmas

DedekindDomain

Ideal

Basic

Lemmas

AdicValuation

Basic

Dvr

IntegralClosure

Derivation

Basic

DiscreteValuationRing

Basic

TFAE

Finiteness

Basic

Bilinear

Cardinality

Cofinite

Defs

Finsupp

Ideal

Lattice

Nakayama

Prod

Projective

Small

Subalgebra

Flat

FaithfullyFlat

Algebra

Basic

Basic

Localization

Stability

FractionalIdeal

Basic

Inverse

Operations

GradedAlgebra

Homogeneous

Ideal

Submodule

Basic

HahnSeries

Addition

Basic

Multiplication

PowerSeries

Summable

Ideal

MinimalPrime

Basic

Localization

Quotient

HasFiniteQuotients

Basic

Basic

Defs

Nilpotent

Noetherian

Operations

PowTransition

Basic

BigOperators

Colon

Cotangent

Defs

GoingDown

GoingUp

IsPrimary

Lattice

Maps

Maximal

Nonunits

Oka

Operations

Over

Pointwise

Prime

Prod

Span

Int

Basic

IntegralClosure

Algebra

Basic

Defs

IsIntegral

Basic

Defs

IsIntegralClosure

Basic

Defs

IntegrallyClosed

Jacobson

Ideal

Polynomial

Radical

Ring

Semiprimary

KrullDimension

Basic

Zero

LocalProperties

Basic

Exactness

IntegrallyClosed

Submodule

LocalRing

MaximalIdeal

Basic

Defs

ResidueField

Basic

Defs

Ideal

RingHom

Basic

Basic

Defs

Localization

AtPrime

Basic

Away

Basic

Algebra

AsSubring

BaseChange

Basic

Defs

FractionRing

Ideal

Integer

Integral

LocalizationLocalization

Module

NumDen

Submodule

MvPolynomial

Symmetric

Defs

Basic

Homogeneous

Tower

WeightedHomogeneous

MvPowerSeries

Basic

Inverse

LexOrder

NoZeroDivisors

Order

Nilpotent

Basic

Defs

Lemmas

Noetherian

Basic

Defs

Orzech

UniqueFactorizationDomain

NonUnitalSubring

Basic

Defs

NonUnitalSubsemiring

Basic

Defs

Norm

Basic

Defs

Transitivity

OreLocalization

Basic

NonZeroDivisors

OreSet

Ring

Polynomial

Cyclotomic

Basic

Eval

Expand

Roots

Eisenstein

Basic

Criterion

Basic

Bernstein

Content

DegreeLT

GaussLemma

Ideal

IntegralNormalization

Nilpotent

Pochhammer

Quotient

RationalRoot

ScaleRoots

SeparableDegree

Subring

Tower

UniqueFactorization

Vieta

PowerSeries

Basic

Inverse

NoZeroDivisors

Order

Trunc

Radical

Basic

RootsOfUnity

AlgebraicallyClosed

Basic

Complex

EnoughRootsOfUnity

Minpoly

PrimitiveRoots

SimpleModule

Basic

SimpleRing

Basic

Defs

Matrix

Spectrum

Maximal

Basic

Defs

Localization

Prime

Basic

Chevalley

ChevalleyComplexity

ConstructibleSet

Defs

Polynomial

RingHom

Topology

TensorProduct

Basic

Finite

Free

Maps

MonoidAlgebra

MvPolynomial

Quotient

Trace

Basic

Defs

TwoSidedIdeal

Basic

Kernel

Lattice

Operations

UniqueFactorizationDomain

Basic

Defs

FactorSet

Finite

GCDMonoid

Ideal

Multiplicity

Nat

NormalizedFactors

Valuation

Discrete

Basic

ValuativeRel

Basic

Basic

ExtendToLocalization

Integers

IsTrivialOn

PrimeMultiplicity

ValuationRing

ValuationSubring

ZMod (file)

Torsion

AdjoinRoot

AlgebraTower

Bezout

Binomial

ChainOfDivisors

EssentialFiniteness

EuclideanDomain

Filtration

FiniteLength

FinitePresentation

FiniteStability

FiniteType

FreeCommRing

FreeRing

Idempotents

IntegralDomain

IsPrimary

IsTensorProduct

LaurentSeries

Length

MatrixAlgebra

MatrixPolynomialAlgebra

Multiplicity

Nakayama

Nullstellensatz

OrzechProperty

PolynomialAlgebra

PowerBasis

PrincipalIdealDomain

PrincipalIdealDomainOfPrime

ReesAlgebra

RingHomProperties

SurjectiveOnStalks

SetTheory

Cardinal

Cofinality

Basic

Enum

Ordinal

Aleph

Arithmetic

Basic

Continuum

Defs

ENNReal

ENat

Finite

Finsupp

NatCard

Order

Ordinal

Pigeonhole

Rat

Regular

SchroederBernstein

Subfield

ToNat

Ordinal

Arithmetic

Basic

Enum

Exponential

Family

FixedPoint

FundamentalSequence

Principal

Univ

Tactic (file)

Algebra

AlgebraNF

Basic

Lemmas

ArithMult (file)

Init

Attr

Core

Register

Basify (file)

Attr

Bound (file)

Attribute

Init

CancelDenoms (file)

Core

CategoryTheory

Bicategory

Basic

Datatypes

Normalize

PureCoherence

Coherence (file)

Basic

Datatypes

Normalize

PureCoherence

Monoidal

Basic

Datatypes

Normalize

PureCoherence

BicategoricalComp

BicategoryCoherence

CancelIso

CategoryStar

CheckCompositions

Elementwise

IsoReassoc

Map

MonoidalComp

Reassoc

Slice

ToApp

ClickSuggestions (file)

Apply

ApplyAt

FindPremises

GRewrite

Rewrite

SectionState

TryPremises

Unfold

Util

ComputeAsymptotics

Multiseries

Monomial

Basic

Predicates

Basic

Basis

Corecursion

Defs

Majorized

Trimming

Lemmas

Continuity (file)

Init

Determinant

Bird

Cert

Meta

Echelon

Bareiss

Cert

Core

Rat

Zsqrtd

Explode (file)

Datatypes

Pretty

FieldSimp (file)

Attr

Discharger

Lemmas

Finiteness (file)

Attr

FunProp (file)

Attr

Core

Decl

Elab

FunctionData

Mor

Theorems

ToBatteries

Types

GCongr (file)

Core

CoreAttrs

ForwardAttr

GRewrite (file)

Core

Elab

Inclusion

Core

Core

DiscrTreeExt

Elab

Expr

Extensions

Inclusion

ToSet

Types

Extension

Core

Core

Init

IntervalDyadicReal

Basic

BinarySplit

Hypotheses

Init

Rational

Tactic

Interval

ExtensionAPI

Attr

Basic

Linarith (file)

Oracle

SimplexAlgorithm (file)

Datatypes

Gauss

PositiveVector

SimplexAlgorithm

FourierMotzkin

Datatypes

Frontend

Lemmas

NNRealPreprocessor

Parsing

Preprocessing

Verification

LinearCombination (file)

Lemmas

Linter (file)

TextBased (file)

UnicodeLinter

AuxLemma

CommandRanges

DeprecatedModule

DeprecatedSyntaxLinter

DirectoryDependency

DocPrime

DocString

EmptyLine

FindDeprecations

FlexibleLinter

GlobalAttributeIn

HashCommandLinter

HaveILetI

HaveLetLinter

Header

InternalConstructor

Lint

MinImports

Multigoal

OldObtain

OverlappingInstances

PPRoundtrip

PrivateModule

Style

TacticDocumentation

UnusedInstancesInType

UnusedTactic

UnusedTacticExtension

UpstreamableDecl

ValidatePRTitle

Whitespace

Matrix

ListMatrix

MulExpand

OfLists

Parsing

Measurability (file)

Init

Monotonicity (file)

Attr

Basic

Lemmas

Nontriviality (file)

Core

NormNum (file)

Abs

Basic

BigOperators

Core

DivMod

Eq

GCD

Ineq

Inv

Irrational

IsCoprime

IsSquare

LegendreSymbol

ModEq

NatFactorial

NatFib

NatLog

NatSqrt

OfScientific

Ordinal

Parity

Pow

PowMod

Prime

RealSqrt

Result

Order (file)

Graph

Basic

Tarjan

CollectFacts

Preprocessing

ToInt

Polynomial

Basic

Core

Positivity (file)

Basic

Core

Finset

Push (file)

Attr

ReduceModChar (file)

Ext

Relation

Rfl

Symm

Ring (file)

Basic

Common

Compare

NamePolyVars

NamePowerVars

PNat

RingNF

Sat

FromLRAT

Simproc

Divisors

ExistsAndEq

Factors

FinsetInterval

VecPerm

Simps (file)

Basic

NotationClass

TacticAnalysis (file)

Declarations

Translate

Attributes

Core

Expr

GuessName

Reorder

TagUnfoldBoundary

ToAdditive

ToDual

UnfoldBoundary

Widget

Calc

CommDiag

CongrM

Conv

GCongr

LibraryRewrite

SelectInsertParamsClass

SelectPanelUtils

StringDiagram

Abel

AdaptationNote

AddGroup

Algebraize

ApplyAt

ApplyCongr

ApplyFun

ApplyWith

Assume

BDSimp

Basic

ByCases

ByContra

Cases

CasesM

Change

Check

Choose

Clean

ClearExcept

ClearExclamation

Clear_

Coe

Common

ComputeDegree

CongrExclamation

CongrM

Constructor

ContinuousFunctionalCalculus

Contrapose

Conv

Convert

Core

CrossRefAttribute

DSimpPercent

DeclarationNames

DefEqAbuse

DefEqTransformations

DepRewrite

DeprecateTo

DeriveCountable

DeriveEncodable

DeriveFintype

DeriveTraversable

DuplicateDecls

ENatToNat

Eqns

ErwQuestion

Eval

ExistsI

Ext

ExtendDoc

ExtractGoal

FBinop

FailIfNoProgress

FastInstance

Field

FinCases

Find

FindSyntax

Generalize

GrindAttrs

Group

GuardGoalNums

GuardHypNums

Have

HaveI

HigherOrder

Hint

ITauto

InferParam

Inhabit

IntervalCases

IrreducibleDef

Lemma

Lift

LinearCombinationPrime

MinImports

MkIffOfInductiveProp

ModCases

Module

ModuleNF

MoveAdd

NoncommRing

NormDet

NormMatMul

NormRank

NthRewrite

Observe

OfNat

PNatToNat

PPWithUniv

Peel

Polyrith

ProdAssoc

ProxyType

Qify

RSuffices

Recover

Rename

RenameBVar

Replace

Rify

Says

ScopedNS

Set

SetLike

SetNotationForOrder

Setm

SimpIntro

SimpLibraryNote

SimpRw

SplitIfs

Spread

StacksAttribute

Subsingleton

Substs

SuccessIfFailWithMsg

SudoSetOption

SuppressCompilation

SwapVar

TFAE

Tauto

TautoSet

TermCongr

ToAdditive

ToDual

ToExpr

ToFun

ToLevel

Trace

TryThis

TypeCheck

TypeStar

UnsetOption

Use

Variable

WLOG

WithoutCDot

Zify

Topology

Algebra

Algebra (file)

Equiv

Group

Basic

ClosedSubgroup

Compact

ContinuousDiv

ContinuousInv

Defs

GroupTopology

Neighborhood

Order

Pointwise

Quotient

Subgroup

Torsor

Units

ZPow

InfiniteSum

Basic

Constructions

Defs

ENNReal

Group

Module

NatInt

Order

Real

Ring

SummationFilter

IsUniformGroup

Basic

Constructions

Defs

Order

MetricSpace

Lipschitz

Module

Alternating

Basic

Topology

ContinuousLinearMap

Basic

Extend

Idempotent

Invertible

PiProd

Quotient

Restrict

RestrictScalars

Equiv

Basic

Pi

Prod

Multilinear

Basic

Bounded

Topology

Spaces

CharacterSpace

ContinuousLinearMap

UniformConvergenceCLM

WeakBilin

WeakDual

Basic

ClosedSubmodule

Complement

Determinant

FiniteDimension

LocallyConvex

ModuleTopology

PerfectPairing

PerfectSpace

Simple

Star

UniformConvergence

Monoid (file)

Defs

FunOnFinite

Nonarchimedean

Bases

Basic

Order

Archimedean

Field

Floor

Group

LiminfLimsup

Ring

Basic

Ideal

Real

SeparationQuotient

Basic

FiniteDimensional

Section

Star (file)

Real

ValuativeRel

Completion

ValuativeTopology

Valued

ValuationTopology

ValuedField

WithVal

Affine

AffineSubspace

ConstMulAction

Constructions

ContinuousAffineEquiv

ContinuousAffineMap

ContinuousMonoidHom

Equicontinuity

Field

FilterBasis

GroupCompletion

GroupWithZero

Indicator

LinearMapCompletion

LinearTopology

MulAction

NonUnitalAlgebra

NonUnitalStarAlgebra

OpenSubgroup

Polynomial

Semigroup

StarSubalgebra

Support

UniformConvergence

UniformField

UniformFilterBasis

UniformMulAction

UniformRing

WithZeroTopology

Baire

CompleteMetrizable

Lemmas

Bornology

Absorbs

Basic

BoundedOperation

Constructions

Hom

Real

Category

TopCat

Limits

Basic

Konig

Adjunctions

Basic

Compactness

Bases

Compact

CompactlyCoherentSpace

Lindelof

LocallyCompact

LocallyFinite

NhdsKer

SigmaCompact

Connected

Basic

Clopen

LocallyConnected

LocallyPathConnected

PathConnected

TotallyDisconnected

Constructions (file)

SumProd

ContinuousMap

Bounded

Basic

Normed

Star

Algebra

Basic

CocompactMap

Compact

ContinuousMapZero

ContinuousSqrt

Defs

Lattice

Ordered

Polynomial

Star

StarOrdered

StoneWeierstrass

Units

Weierstrass

Covering

AddCircle

Basic

Quotient

Defs

Basic

Filter

Induced

Sequences

Ultrafilter

EMetricSpace

Basic

BoundedVariation

Defs

Diam

Lipschitz

MulOpposite

Pi

VariationOnFromTo

FiberBundle

Basic

IsHomeomorphicTrivialBundle

Trivialization

GDelta

Basic

MetrizableSpace

Hom

ContinuousEval

ContinuousEvalConst

Homeomorph

Defs

Lemmas

Quotient

TransferInstance

Instances

AddCircle

Defs

Real

ENNReal

Lemmas

EReal

Lemmas

NNReal

Lemmas

Real

Lemmas

Discrete

Int

Matrix

Nat

Rat

RealVectorSpace

Sign

ZMultiples

LocallyConstant

Basic

Maps

Proper

Basic

CompactlyGenerated

Strict

Basic

Basic

OpenQuotient

MetricSpace

ProperSpace (file)

Real

Pseudo

Basic

Constructions

Defs

Lemmas

Pi

Real

Algebra

Antilipschitz

Basic

Bounded

CantorScheme

CauSeqFilter

Cauchy

Completion

Contracting

Defs

Dilation

DilationEquiv

Equicontinuity

Gluing

HausdorffDistance

IsometricSMul

Isometry

Lipschitz

Perfect

PiNat

Polish

ThickenedIndicator

Thickening

UniformConvergence

Metrizable

Basic

CompletelyMetrizable

Real

Uniformity

Urysohn

OpenPartialHomeomorph

Basic

Composition

Constructions

Continuity

Defs

IsImage

Order (file)

AtTopBotIxx

Basic

Bornology

Compact

DenselyOrdered

ExtendFrom

IntermediateValue

IsLUB

IsLocallyClosed

Lattice

LeftRight

LeftRightLim

LeftRightNhds

LiminfLimsup

LocalExtr

Monotone

MonotoneContinuity

MonotoneConvergence

OrderClosed

ProjIcc

Real

Rolle

T5

PartialHomeomorph

Basic

Defs

Semicontinuity

Basic

Defs

Hemicontinuity

Separation

Basic

CountableSeparatingOn

GDelta

Hausdorff

Regular

SeparatedNhds

Sets

Closeds

Compacts

OpenCover

Opens

VietorisTopology

Spectral

Basic

Hom

Prespectral

UniformSpace

AbstractCompletion

Basic

Cauchy

Closeds

Compact

CompactConvergence

CompleteSeparated

Completion

Defs

DiscreteUniformity

Equicontinuity

Equiv

HeineCantor

LocallyUniformConvergence

Matrix

OfFun

Pi

Real

Separation

UniformApproximation

UniformConvergence

UniformConvergenceTopology

UniformEmbedding

AlexandrovDiscrete

Bases

Basic

Clopen

Closure

ClusterPt

Coherent

CompactOpen

Constructible

Continuous

ContinuousOn

DenseEmbedding

DiscreteSubset

ExtendFrom

IndicatorConstPointwise

Inseparable

Irreducible

IsLocalHomeomorph

KrullDimension

LocalAtTarget

LocallyClosed

LocallyFinite

Neighborhoods

NhdsKer

NhdsSet

NhdsWithin

NoetherianSpace

Path

Perfect

Piecewise

QuasiSeparated

SeparatedMap

Sequences

Sober

Ultrafilter

UnitInterval

UrysohnsLemma

WithTopology

Util

AtomM (file)

Recurse

CodeActions (file)

BinderPlicity

AddRelatedDecl

AtLocation

CompileInductive

CountHeartbeats

DelabNonCanonical

Delaborators

DischargerAsTactic

ElabWithoutMVars

Notation3

PPOptions

ParseCommand

PrintSorries

Qq

Superscript

SynthesizeUsing

Tactic

TermReduce

TransImports

WhatsNew

WithWeakNamespace

Init

Plausible (file)

Arbitrary

ArbitraryFueled

Attr

DeriveArbitrary

DeriveShrinkable

Functions

Gen

Random

Sampleable

Shrinkable

Tactic

Testable

ProofWidgets

Component

Panel

Basic

Basic

FilterDetails

HtmlDisplay

MakeEditLink

OfRpcMethod

PenroseDiagram

RefreshComponent

Data

Html

Presentation

Expr

Cancellable

Compat

Util

Qq (file)

ForLean

Do

ReduceEval

ToExpr

AssertInstancesCommute

Commands

Delab

Macro

Match

MatchImpl

MetaM

Simp

SortLocalDecls

Typ

Std (file)

Async (file)

Basic

ContextAsync

DNS

IO

Process

Select

Signal

System

TCP

Timer

UDP

Data (file)

DHashMap (file)

Internal

AssocList

Basic

Iterator

Lemmas

Defs

HashesTo

Index

Model

Raw

RawLemmas

WF

AdditionalOperations

Basic

DecidableEquiv

Iterator

IteratorLemmas

Lemmas

Raw

RawDecidableEquiv

RawDef

RawLemmas

DTreeMap (file)

Internal

WF

Defs

Lemmas

Balanced

Balancing

Cell

Def

Lemmas

Model

Operations

Ordered

Queries

Zipper

Raw (file)

AdditionalOperations

Basic

DecidableEquiv

Iterator

Lemmas

Slice

WF

AdditionalOperations

Basic

DecidableEquiv

Iterator

Lemmas

Slice

ExtDHashMap (file)

Basic

Lemmas

ExtDTreeMap (file)

Basic

Lemmas

ExtHashMap (file)

Basic

Lemmas

ExtHashSet (file)

Basic

Lemmas

ExtTreeMap (file)

Basic

Lemmas

ExtTreeSet (file)

Basic

Lemmas

HashMap (file)

AdditionalOperations

Basic

DecidableEquiv

Iterator

IteratorLemmas

Lemmas

Raw

RawDecidableEquiv

RawLemmas

HashSet (file)

Basic

DecidableEquiv

Iterator

IteratorLemmas

Lemmas

Raw

RawDecidableEquiv

RawLemmas

Internal

List

Associative

Defs

Cut

Iterators (file)

Combinators (file)

Monadic (file)

Drop

DropWhile

StepSize

TakeWhile

Zip

Drop

DropWhile

StepSize

TakeWhile

Zip

Consumers (file)

Monadic (file)

Set

Set

Lemmas (file)

Combinators (file)

Monadic (file)

Drop

DropWhile

FilterMap

TakeWhile

Zip

Drop

DropWhile

TakeWhile

Zip

Consumers (file)

Monadic (file)

Collect

Loop

Set

Collect

Loop

Set

Equivalence (file)

Basic

HetT

StepCongr

Producers (file)

Monadic (file)

Array

Empty

List

Vector

Array

Empty

Range

Repeat

Slice

Vector

Monadic

Producers (file)

Monadic (file)

Array

Empty

Vector

Array

Empty

Range

Repeat

Slice

Vector

String (file)

ToInt

ToNat

TreeMap (file)

Raw (file)

AdditionalOperations

Basic

DecidableEquiv

Iterator

Lemmas

Slice

WF

AdditionalOperations

Basic

DecidableEquiv

Iterator

Lemmas

Slice

TreeSet (file)

Raw (file)

Basic

DecidableEquiv

Iterator

Lemmas

Slice

WF

AdditionalOperations

Basic

DecidableEquiv

Iterator

Lemmas

Slice

ByteSlice

Do (file)

Internal (file)

Ensures (file)

Def

Lemmas

SPred (file)

Notation (file)

Basic

DerivedLaws

Laws

SPred

SVal

Triple (file)

Basic

SpecLemmas

WP (file)

Basic

Monad

SimpLemmas

Sound

PostCond

PredTrans

Http (file)

Data (file)

Body (file)

Any

Basic

Empty

Full

Length

Replayable

Stream

Headers (file)

Basic

Name

Value

URI (file)

Basic

Config

Encoding

Parser

Chunk

Extensions

Method

Request

Response

Status

Version

Internal (file)

Char

ChunkedBuffer

Encode

IndexMultiMap

LowerCase

String

Protocol

H1 (file)

Config

Error

Event

Message

Parser

Reader

Redirect

Writer

Server (file)

Config

Connection

Handler

Test

Helpers

Transport

Internal (file)

ForIn (file)

Basic

Lemmas

Order

Basic

FrameClosure

Heyting

Instances

Lemmas

OfProp

PredTrans

PreservesSup

PropLattice

Parsec (file)

Basic

ByteArray

String

UV (file)

DNS

Loop

Signal

System

TCP

Timer

UDP

Net (file)

Addr

Sat (file)

AIG (file)

RefVecOperator (file)

Fold

Map

Zip

Basic

CNF

Cached

CachedGates

CachedGatesLemmas

CachedLemmas

If

LawfulOperator

LawfulVecOperator

Lemmas

RefVec

Relabel

RelabelNat

CNF (file)

Basic

Dimacs

Entails

Literal

Negation

Redundancy

Relabel

RelabelFin

Sat

SpecLemmas

Unit

Sync (file)

Barrier

Basic

Broadcast

CancellationContext

CancellationToken

Channel

Mutex

Notify

RecursiveMutex

Semaphore

SharedMutex

StreamMap

Tactic (file)

BVDecide (file)

Bitblast (file)

BVExpr (file)

Circuit (file)

Impl (file)

Operations

Add

Append

Clz

Cpop

Eq

Extract

GetLsbD

Mul

Neg

Not

Replicate

Reverse

RotateLeft

RotateRight

ShiftLeft

ShiftRight

Sub

Udiv

Ult

Umod

ZeroExtend

Carry

Const

Expr

Pred

Substructure

Var

Lemmas (file)

Operations

Add

Append

Clz

Cpop

Eq

Extract

GetLsbD

Mul

Neg

Not

Replicate

Reverse

RotateLeft

RotateRight

ShiftLeft

ShiftRight

Sub

Udiv

Ult

Umod

ZeroExtend

Basic

Carry

Const

Expr

Pred

Var

Basic

BoolExpr (file)

Basic

LRAT (file)

Internal (file)

Add

Assignment

Basic

Checker

Delete

Empty

Rat

Rup

Actions

Checker

Parser

Normalize (file)

BitVec

Bool

Canonicalize

Equal

Prop

Reflect

Syntax

Do (file)

ProofMode

Syntax

Time (file)

Date (file)

Unit

Basic

Day

Month

Week

Weekday

Year

Basic

PlainDate

ValidDate

DateTime (file)

PlainDateTime

Timestamp

WallTime

Format (file)

Basic

DateFormat

Modifier

Internal (file)

Bounded

UnitVal

Notation (file)

Spec

Time (file)

Unit

Basic

Hour

Millisecond

Minute

Nanosecond

Second

Basic

HourMarker

PlainTime

Zoned (file)

Database (file)

Basic

PosixTz

TZdb

TzIf

Windows

RecurringRule

TimeZone

ZoneRules

Duration

WP (file)

Gadget

Assert

ForIn

Monad (file)

Basic

Conjunctive

Frame

Instances

Lemmas

Sound

Triple (file)

Basic

Conjunctive

Monad

SpecLemmas

Assertion

Basic

Conjunctive

EStack

Frame

Color scheme

darksystemlight