Enum BlockType 

pub enum BlockType {
    SuspectedTypo {
        found: Symbol,
        suggestion: Symbol,
    },
    Theorem,
    Main,
    Definition,
    Define,
    Axiom,
    Theory,
    Proof,
    Example,
    Logic,
    Note,
    Function,
    TypeDef,
    Policy,
    Requires,
    Hardware,
    Property,
    No,
    Tier,
}

Document structure block type markers.

LOGOS uses markdown-style ## Header syntax to delimit different sections of a program or proof document.

Variants

SuspectedTypo

An unknown ## Header a small edit distance from a CONSEQUENTIAL code header (## Mian → Main) — the parser fails loudly with the suggestion instead of silently treating the whole block as prose.

Fields

found: Symbol

suggestion: Symbol

Theorem

## Theorem - Declares a proposition to be proved.

Main

## Main - Program entry point for imperative code.

Definition

## Definition - Introduces new terminology or type definitions.

Define

## Define - Mints a vernacular-logic predicate definition that the prover unfolds (Rung 0a). Distinct from ## Definition (type defs).

Axiom

## Axiom - Declares a named first-order axiom in formal notation (## Axiom name: for all a b, Cong(a,b,b,a).). Its body is parsed by the formal-formula parser and registered as a shared premise for later theorems — the seam for an axiomatic base like Tarski geometry.

Theory

## Theory - Names a development that groups the ## Axioms and ## Theorems that follow it (## Theory Tarski).

Proof

## Proof - Contains proof steps for a theorem.

Example

## Example - Illustrative examples.

Logic

## Logic - Direct logical notation input.

Note

## Note - Explanatory documentation.

Function

## To - Function definition block.

TypeDef

Inline type definition: ## A Point has: or ## A Color is one of:.

Policy

## Policy - Security policy rule definitions.

Requires

## Requires - External crate dependency declarations.

Hardware

## Hardware - Signal declarations for hardware verification.

Property

## Property - Temporal assertions for hardware verification.

No

## No - Optimization annotation (followed by Memo, TCO, Peephole, Borrow, or Optimize).

Tier

## Tier - Tiered-optimizer pin: ## Tier <opt> <eager|t1|t2|t3|never> overrides the hotness tier at which that optimization runs (HOTSWAP §8).

Trait Implementations

impl Clone for BlockType

fn clone(&self) -> BlockType

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for BlockType

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl PartialEq for BlockType

fn eq(&self, other: &BlockType) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Copy for BlockType

impl Eq for BlockType

impl StructuralPartialEq for BlockType