Module literate_parser 

Literate Specification Parser for the Kernel.

This module parses English-like “Literate” syntax and emits the same Command and Term structures as the Coq-style parser.

Supported Syntax

Inductive Types

A Bool is either Yes or No.
A Nat is either:
    Zero.
    a Successor with pred: Nat.

Function Definitions (with implicit recursion)

## To add (n: Nat) and (m: Nat) -> Nat:
    Consider n:
        When Zero: Yield m.
        When Successor k: Yield Successor (add k m).

Pattern Matching

Consider x:
    When Zero: Yield 0.
    When Successor k: Yield k.

Lambda Expressions

given x: Nat yields Successor x
|x: Nat| -> Successor x

Functions

parse_definition

Parse “## To [name] (params) -> RetType:” into Command::Definition

parse_inductive

Parse “A [Name] is either…” into Command::Inductive

parse_let_definition

Parse “Let [name] be [term].” into Command::Definition (constant, not function)

parse_theorem

Parse “## Theorem: [name] Statement: [proposition].” into Command::Definition