Models Reference¶

API Models¶

api ¶

Pydantic models for API data interchange.

This module defines the Pydantic models that represent the structure of request and response bodies for the remote Lean Explore API. These models are used by the API client for data validation and serialization.

Classes¶

APICitationsResponse ¶

Bases: BaseModel

Represents the response structure for a dependencies (citations) API call.

Attributes:

Name	Type	Description
`source_group_id`	`int`	ID of the statement group for which citations were requested.
`citations`	`List[APISearchResultItem]`	A list of statement groups that are cited by the source group.
`count`	`int`	The number of citations found and returned.

APIPrimaryDeclarationInfo ¶

Bases: BaseModel

Minimal information about a primary declaration within an API response.

Attributes:

Name	Type	Description
`lean_name`	`Optional[str]`	The Lean name of the primary declaration, if available.

APISearchResponse ¶

Bases: BaseModel

Represents the complete response structure for a search API call.

Attributes:

Name	Type	Description
`query`	`str`	The original search query string submitted by the user.
`packages_applied`	`Optional[List[str]]`	List of package filters applied to the search, if any.
`results`	`List[APISearchResultItem]`	A list of search result items.
`count`	`int`	The number of results returned in the current response.
`total_candidates_considered`	`int`	The total number of potential candidates considered by the search algorithm before limiting results.
`processing_time_ms`	`int`	Server processing time for search request, in milliseconds.

APISearchResultItem ¶

Bases: BaseModel

Represents a single statement group item as returned by API endpoints.

This model is used for items in search results and for the direct retrieval of a statement group by its ID.

Attributes:

Name	Type	Description
`id`	`int`	The unique identifier of the statement group.
`primary_declaration`	`APIPrimaryDeclarationInfo`	Information about the primary declaration.
`source_file`	`str`	The source file where the statement group is located.
`range_start_line`	`int`	Start line of statement group in source file.
`display_statement_text`	`Optional[str]`	Display-friendly statement text, if available.
`statement_text`	`str`	The full canonical statement text.
`docstring`	`Optional[str]`	The docstring associated with the statement group, if available.
`informal_description`	`Optional[str]`	Informal description of the statement group, if available.

Database Models¶

db ¶

SQLAlchemy ORM models for the lean_explore database.

Defines 'declarations', 'dependencies', 'statement_groups', and 'statement_group_dependencies' tables representing Lean entities, their dependency graphs at different granularities, and source code groupings. Uses SQLAlchemy 2.0 syntax.

Classes¶

Base ¶

Bases: DeclarativeBase

Base class for SQLAlchemy declarative models.

Includes metadata with naming conventions for database constraints and indexes, ensuring consistency across the database schema.

Declaration ¶

Bases: Base

Represents a Lean declaration, a node in the dependency graph.

Stores information about Lean declarations (definitions, theorems, axioms, etc.), including source location, Lean code, and descriptions. Declarations from the same source block can be grouped via statement_group_id.

Attributes:

Name	Type	Description
`id`	`Mapped[int]`	Primary key identifier.
`lean_name`	`Mapped[str]`	Fully qualified Lean name (e.g., 'Nat.add'), unique and indexed.
`decl_type`	`Mapped[str]`	Type of declaration (e.g., 'theorem', 'definition').
`source_file`	`Mapped[Optional[str]]`	Relative path to the .lean source file.
`module_name`	`Mapped[Optional[str]]`	Lean module name (e.g., 'Mathlib.Data.Nat.Basic'), indexed.
`is_internal`	`Mapped[bool]`	True if considered compiler-internal or auxiliary.
`docstring`	`Mapped[Optional[str]]`	Documentation string, if available.
`is_protected`	`Mapped[bool]`	True if marked 'protected' in Lean.
`is_deprecated`	`Mapped[bool]`	True if marked 'deprecated'.
`is_projection`	`Mapped[bool]`	True if it's a projection (e.g., from a class/structure).
`range_start_line`	`Mapped[Optional[int]]`	Starting line number of the source block.
`range_start_col`	`Mapped[Optional[int]]`	Starting column number of the source block.
`range_end_line`	`Mapped[Optional[int]]`	Ending line number of the source block.
`range_end_col`	`Mapped[Optional[int]]`	Ending column number of the source block.
`statement_text`	`Mapped[Optional[str]]`	Full Lean code text of the originating source block.
`declaration_signature`	`Mapped[Optional[str]]`	Extracted Lean signature text of the declaration.
`statement_group_id`	`Mapped[Optional[int]]`	Optional foreign key to `statement_groups.id`.
`pagerank_score`	`Mapped[Optional[float]]`	PageRank score within the dependency graph, indexed.
`created_at`	`Mapped[datetime]`	Timestamp of record creation.
`updated_at`	`Mapped[datetime]`	Timestamp of last record update.
`statement_group`	`Mapped[Optional[StatementGroup]]`	SQLAlchemy relationship to the StatementGroup.

Functions¶

repr ¶

__repr__()

Provides a developer-friendly string representation.

Source code in src/lean_explore/shared/models/db.py

def __repr__(self) -> str:
    """Provides a developer-friendly string representation."""
    group_id_str = (
        f", group_id={self.statement_group_id}" if self.statement_group_id else ""
    )
    return (
        f"<Declaration(id={self.id}, lean_name='{self.lean_name}', "
        f"type='{self.decl_type}'{group_id_str})>"
    )

Dependency ¶

Bases: Base

Represents a dependency link between two Lean declarations.

Each row signifies that a 'source' declaration depends on a 'target' declaration, forming an edge in the dependency graph. The nature of this dependency is described by dependency_type.

Attributes:

Name	Type	Description
`id`	`Mapped[int]`	Primary key identifier for the dependency link.
`source_decl_id`	`Mapped[int]`	Foreign key to the `Declaration` that depends on another.
`target_decl_id`	`Mapped[int]`	Foreign key to the `Declaration` that is depended upon.
`dependency_type`	`Mapped[str]`	String describing the type of dependency (e.g., 'Direct').
`created_at`	`Mapped[datetime]`	Timestamp of record creation.

Functions¶

repr ¶

__repr__()

Provides a developer-friendly string representation.

Source code in src/lean_explore/shared/models/db.py

def __repr__(self) -> str:
    """Provides a developer-friendly string representation."""
    return (
        f"<Dependency(id={self.id}, source={self.source_decl_id}, "
        f"target={self.target_decl_id}, type='{self.dependency_type}')>"
    )

StatementGroup ¶

Bases: Base

Represents a unique block of source code text.

This table groups multiple Declaration entries that originate from the exact same source code text and location. This allows search results to show a single entry for a code block, while retaining all individual declarations for graph analysis and detailed views. It also tracks dependencies to and from other statement groups.

Attributes:

Name	Type	Description
`id`	`Mapped[int]`	Primary key identifier for the statement group.
`text_hash`	`Mapped[str]`	SHA-256 hash of `statement_text` for unique identification.
`statement_text`	`Mapped[str]`	Canonical source code text for this group (full block).
`display_statement_text`	`Mapped[Optional[str]]`	Optional, potentially truncated version of the source code, optimized for display (e.g., omitting proofs).
`docstring`	`Mapped[Optional[str]]`	Docstring associated with this code block, typically from the primary declaration.
`informal_description`	`Mapped[Optional[str]]`	Optional informal English description, potentially LLM-generated.
`informal_summary`	`Mapped[Optional[str]]`	Optional informal English summary, potentially LLM-generated.
`source_file`	`Mapped[str]`	Relative path to the .lean file containing this block.
`range_start_line`	`Mapped[int]`	Starting line number of the block in the source file.
`range_start_col`	`Mapped[int]`	Starting column number of the block.
`range_end_line`	`Mapped[int]`	Ending line number of the block.
`range_end_col`	`Mapped[int]`	Ending column number of the block.
`pagerank_score`	`Mapped[Optional[float]]`	PageRank score calculated for this statement group.
`scaled_pagerank_score`	`Mapped[Optional[float]]`	Log-transformed, min-max scaled PageRank score.
`primary_decl_id`	`Mapped[int]`	Foreign key to the 'declarations' table, identifying the primary or most representative declaration of this group.
`created_at`	`Mapped[datetime]`	Timestamp of when the record was created.
`updated_at`	`Mapped[datetime]`	Timestamp of the last update to the record.
`primary_declaration`	`Mapped[Declaration]`	SQLAlchemy relationship to the primary Declaration.
`declarations`	`Mapped[List[Declaration]]`	SQLAlchemy relationship to all Declarations in this group.
`dependencies_as_source`	`Mapped[List[StatementGroupDependency]]`	Links to `StatementGroupDependency` where this group is the source (i.e., this group depends on others).
`dependencies_as_target`	`Mapped[List[StatementGroupDependency]]`	Links to `StatementGroupDependency` where this group is the target (i.e., other groups depend on this one).

Functions¶

repr ¶

__repr__()

Provides a developer-friendly string representation.

Source code in src/lean_explore/shared/models/db.py

def __repr__(self) -> str:
    """Provides a developer-friendly string representation."""
    has_desc = "+" if self.informal_description else "-"
    return (
        f"<StatementGroup(id={self.id}, hash='{self.text_hash[:8]}...', "
        f"primary_decl_id='{self.primary_decl_id}', informal_desc='{has_desc}', "
        f"loc='{self.source_file}:{self.range_start_line}:{self.range_start_col}')>"
    )

StatementGroupDependency ¶

Bases: Base

Represents a dependency link between two StatementGroups.

Each row signifies that a 'source' statement group depends on a 'target' statement group. This allows for a higher-level dependency graph.

Attributes:

Name	Type	Description
`id`	`Mapped[int]`	Primary key identifier for the group dependency link.
`source_statement_group_id`	`Mapped[int]`	Foreign key to the `StatementGroup` that depends on another.
`target_statement_group_id`	`Mapped[int]`	Foreign key to the `StatementGroup` that is depended upon.
`dependency_type`	`Mapped[str]`	String describing the type of group dependency (e.g., 'DerivedFromDecl').
`created_at`	`Mapped[datetime]`	Timestamp of record creation.
`source_group`	`Mapped[StatementGroup]`	SQLAlchemy relationship to the source StatementGroup.
`target_group`	`Mapped[StatementGroup]`	SQLAlchemy relationship to the target StatementGroup.

Functions¶

repr ¶

__repr__()

Provides a developer-friendly string representation.

Source code in src/lean_explore/shared/models/db.py

def __repr__(self) -> str:
    """Provides a developer-friendly string representation."""
    return (
        f"<StatementGroupDependency(id={self.id}, "
        f"source_sg_id={self.source_statement_group_id}, "
        f"target_sg_id={self.target_statement_group_id}, "
        f"type='{self.dependency_type}')>"
    )

Models Reference¶

API Models¶

api ¶

Classes¶

APICitationsResponse ¶

APIPrimaryDeclarationInfo ¶

APISearchResponse ¶

APISearchResultItem ¶

Database Models¶

db ¶

Classes¶

Base ¶

Declaration ¶

Functions¶

__repr__ ¶

Dependency ¶

Functions¶

__repr__ ¶

StatementGroup ¶

Functions¶

__repr__ ¶

StatementGroupDependency ¶

Functions¶

__repr__ ¶

repr ¶

repr ¶

repr ¶

repr ¶