Documentation

GaudisCrypt.Syntax.Syntax

Concrete syntax #

Barrel module for the surface syntax of the language: expressions (ExpressionSyntax.lean), statements and procedures (ProgramSyntax.lean), modules (ModuleSyntax.lean), and Hoare triples (HoareSyntax.lean).

HoareSyntax.lean is the one file here that reaches past Language/ — hoareStmt and hoareProc themselves live in Logic/Hoare.lean — so this barrel pulls that in too. It also imports its sibling ModuleSyntax.lean, the procedure-triple form being about a module.