Enum BlockType 

pub enum BlockType {
    Theorem,
    Main,
    Definition,
    Proof,
    Example,
    Logic,
    Note,
    Function,
    TypeDef,
    Policy,
    Requires,
    Hardware,
    Property,
    No,
}

Document structure block type markers.

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

Variants

Theorem

## Theorem - Declares a proposition to be proved.

Main

## Main - Program entry point for imperative code.

Definition

## Definition - Introduces new terminology or type definitions.

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).

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

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