FPL Syntax Diagrams (Version 1.0.1)

Namespace:


               Namespace
                        ::= CW* NamespaceIdentifier CW* NamespaceBlock CW*

no references

NamespaceBlock:


               NamespaceBlock
                        ::= '{' CW* ExtensionBlock? CW* UsesClause? CW* RulesOfInferenceBlock? CW* TheoryBlock CW* LocalizationBlock? CW* '}'

referenced by:

Namespace

WildcardTheoryNamespaceList:


               WildcardTheoryNamespaceList
                        ::= WildcardTheoryNamespace ( IW? ',' IW? WildcardTheoryNamespace )*

referenced by:

UsesClause

ExtensionBlock:


               ExtensionBlock
                        ::= ExtensionHeader SW ExtensionContent IW? ExtensionTail

referenced by:

NamespaceBlock

ExtensionHeader:


               ExtensionHeader
                        ::= ':' 'ext'

referenced by:

ExtensionBlock

ExtensionContent:


               ExtensionContent
                        ::= regular_expression '/((?!:end).)*/'

referenced by:

ExtensionBlock

ExtensionTail:


               ExtensionTail
                        ::= ':' 'end' SW

referenced by:

ExtensionBlock

UsesClause:


               UsesClause
                        ::= 'uses' SW WildcardTheoryNamespaceList SW

referenced by:

NamespaceBlock

TheoryBlock:


               TheoryBlock
                        ::= TheoryHeader CW* '{' CW* BuildingBlockList? CW* '}'

referenced by:

NamespaceBlock

RulesOfInferenceBlock:


               RulesOfInferenceBlock
                        ::= InferenceHeader CW* '{' CW* RuleOfInferenceList CW* '}'

referenced by:

NamespaceBlock

InferenceHeader:


               InferenceHeader
                        ::= 'inference'
                          | 'inf'

referenced by:

RulesOfInferenceBlock

PremiseHeader:


               PremiseHeader
                        ::= 'premise'
                          | 'pre'

referenced by:

PremiseBlock
PremiseOrOtherPredicate

ConclusionHeader:


               ConclusionHeader
                        ::= 'conclusion'
                          | 'con'

referenced by:

ConclusionBlock

RuleOfInferenceList:


               RuleOfInferenceList
                        ::= RuleOfInference ( CW* RuleOfInference )*

referenced by:

RulesOfInferenceBlock

RuleOfInference:


               RuleOfInference
                        ::= Signature IW? PremiseConclusionBlock

referenced by:

RuleOfInferenceList

PremiseConclusionBlock:


               PremiseConclusionBlock
                        ::= '{' CW* VariableSpecificationList? CW* PremiseBlock CW* ConclusionBlock CW* '}'

referenced by:

RuleOfInference
TheoremLikeStatementOrConjecture

PremiseBlock:


               PremiseBlock
                        ::= PremiseHeader IW? ':' CW* Predicate?

referenced by:

PremiseConclusionBlock

ConclusionBlock:


               ConclusionBlock
                        ::= ConclusionHeader IW? ':' CW* Predicate

referenced by:

PremiseConclusionBlock

TheoryHeader:


               TheoryHeader
                        ::= 'theory'
                          | 'th'

referenced by:

TheoryBlock

BuildingBlockList:


               BuildingBlockList
                        ::= BuildingBlock ( CW* BuildingBlock )*

referenced by:

TheoryBlock

BuildingBlock:


               BuildingBlock
                        ::= Definition
                          | Axiom
                          | TheoremLikeStatementOrConjecture
                          | Proof

referenced by:

BuildingBlockList

Definition:


               Definition
                        ::= DefinitionClass
                          | DefinitionPredicate
                          | DefinitionFunctionalTerm

referenced by:

BuildingBlock

DefinitionClass:


               DefinitionClass
                        ::= ClassHeader SW PredicateIdentifier IW? ':' IW? GeneralType CW* ObjectDefinitionBlock

referenced by:

Definition

ObjectDefinitionBlock:


               ObjectDefinitionBlock
                        ::= '{' CW* VariableSpecificationList? CW* DefinitionContentList? CW* '}'

referenced by:

DefinitionClass

FunctionalTermDefinitionBlock:


               FunctionalTermDefinitionBlock
                        ::= '{' CW* VariableSpecificationList? CW* PropertyList? CW* '}'

referenced by:

DefinitionFunctionalTerm

DefinitionContentList:


               DefinitionContentList
                        ::= DefinitionContent ( CW* DefinitionContent )*

referenced by:

ObjectDefinitionBlock

DefinitionContent:


               DefinitionContent
                        ::= Property
                          | Constructor

referenced by:

DefinitionContentList

DefinitionFunctionalTerm:


               DefinitionFunctionalTerm
                        ::= FunctionalTermSignature CW* FunctionalTermDefinitionBlock

referenced by:

Definition

FunctionalTermSignature:


               FunctionalTermSignature
                        ::= FunctionalTermHeader SW Signature IW? Mapping

referenced by:

DefinitionFunctionalTerm
FunctionalTermInstance

Mapping:


               Mapping  ::= '->' IW? TypeOrTupleOfTypes

referenced by:

FunctionalTermSignature

VariableSpecificationList:


               VariableSpecificationList
                        ::= ( CW* VariableSpecification SW )+

referenced by:

AxiomBlock
FunctionalTermDefinitionBlock
InstanceBlock
ObjectDefinitionBlock
PredicateDefinitionBlock
PremiseConclusionBlock
ProofBlock

VariableSpecification:


               VariableSpecification
                        ::= Statement
                          | NamedVariableDeclaration

referenced by:

VariableSpecificationList

AssertionStatement:


               AssertionStatement
                        ::= 'assert' SW Predicate

referenced by:

Statement

VariableDeclaration:


               VariableDeclaration
                        ::= AnonymousDeclaration
                          | NamedVariableDeclaration

referenced by:

VariableDeclarationList

AnonymousDeclaration:


               AnonymousDeclaration
                        ::= AnonymousSignature
                          | GeneralType

referenced by:

VariableDeclaration

NamedVariableDeclaration:


               NamedVariableDeclaration
                        ::= VariableList IW? ':' IW? VariableType

referenced by:

VariableDeclaration
VariableSpecification

VariableType:


               VariableType
                        ::= AnonymousSignature
                          | GeneralType

referenced by:

CoordInSignature
IsOperator
NamedVariableDeclaration
TypeOrTupleOfTypes

GeneralType:


               GeneralType
                        ::= CallModifier? ( TypeWithCoord | Type | IndexHeader )

referenced by:

AnonymousDeclaration
AnonymousSignature
ClassInstance
DefinitionClass
TupleOfTypes
VariableType

IndexHeader:


               IndexHeader
                        ::= 'index'
                          | 'ind'

referenced by:

GeneralType

Type:


               Type     ::= PredicateIdentifier
                          | XId
                          | PredicateHeader
                          | FunctionalTermHeader
                          | ObjectHeader

referenced by:

GeneralType
TypeWithCoord

VariableList:


               VariableList
                        ::= Variable ( IW? ',' IW? Variable )*

referenced by:

All
Exists
NamedVariableDeclaration
PythonDelegate

TypeOrTupleOfTypes:


               TypeOrTupleOfTypes
                        ::= TupleOfTypes
                          | VariableType

referenced by:

Mapping

TupleOfTypes:


               TupleOfTypes
                        ::= '(' IW? GeneralType ( IW? ',' IW? GeneralType )* ')'

referenced by:

TypeOrTupleOfTypes

DefinitionPredicate:


               DefinitionPredicate
                        ::= PredicateHeader SW Signature CW* PredicateDefinitionBlock

referenced by:

Definition
DefinitionProperty

PredicateHeader:


               PredicateHeader
                        ::= 'predicate'
                          | 'pred'

referenced by:

DefinitionPredicate
Type

FunctionalTermHeader:


               FunctionalTermHeader
                        ::= 'function'
                          | 'func'

referenced by:

FunctionalTermSignature
Type

PredicateDefinitionBlock:


               PredicateDefinitionBlock
                        ::= '{' CW* VariableSpecificationList? CW* Predicate? CW* '}'

referenced by:

DefinitionPredicate

PredicateIdentifier:


               PredicateIdentifier
                        ::= AliasedId
                          | IdStartsWithCap

referenced by:

DefinitionClass
Identifier
ProofIdentifier
ReferencedResultIdentifier
Signature
Type

AliasedId:


               AliasedId
                        ::= IdStartsWithCap ( '.' IdStartsWithCap )+

referenced by:

PredicateIdentifier

ClassHeader:


               ClassHeader
                        ::= 'class'
                          | 'cl'

referenced by:

DefinitionClass

ObjectHeader:


               ObjectHeader
                        ::= 'object'
                          | 'obj'
                          | LongTemplateHeader
                          | TemplateHeader

referenced by:

Type

LongTemplateHeader:


               LongTemplateHeader
                        ::= TemplateHeader ( IdStartsWithCap | Digit )

referenced by:

ObjectHeader

TemplateHeader:


               TemplateHeader
                        ::= 'template'
                          | 'tpl'

referenced by:

LongTemplateHeader
ObjectHeader

Axiom:


               Axiom    ::= AxiomHeader SW Signature CW* AxiomBlock

referenced by:

BuildingBlock

AxiomHeader:


               AxiomHeader
                        ::= 'axiom'
                          | 'ax'
                          | 'postulate'
                          | 'post'

referenced by:

Axiom

AxiomBlock:


               AxiomBlock
                        ::= '{' CW* VariableSpecificationList? CW* Predicate CW* '}'

referenced by:

Axiom

PropertyList:


               PropertyList
                        ::= Property+

referenced by:

FunctionalTermDefinitionBlock

Property:


               Property ::= CW* PropertyHeader SW DefinitionProperty

referenced by:

DefinitionContent
PropertyList

DefinitionProperty:


               DefinitionProperty
                        ::= ClassInstance
                          | DefinitionPredicate
                          | FunctionalTermInstance

referenced by:

Property

ClassInstance:


               ClassInstance
                        ::= GeneralType SW Signature CW* InstanceBlock

referenced by:

DefinitionProperty

FunctionalTermInstance:


               FunctionalTermInstance
                        ::= FunctionalTermSignature CW* InstanceBlock

referenced by:

DefinitionProperty

PropertyHeader:


               PropertyHeader
                        ::= 'mandatory'
                          | 'mand'
                          | 'optional'
                          | 'opt'

referenced by:

Property

Constructor:


               Constructor
                        ::= Signature CW* InstanceBlock

referenced by:

DefinitionContent

InstanceBlock:


               InstanceBlock
                        ::= '{' CW* VariableSpecificationList CW* '}'

referenced by:

ClassInstance
Constructor
FunctionalTermInstance

Signature:


               Signature
                        ::= PredicateIdentifier IW? ParamTuple

referenced by:

Axiom
ClassInstance
Constructor
DefinitionPredicate
FunctionalTermSignature
ReferencedResultIdentifier
RuleOfInference
TheoremLikeStatementOrConjecture

AnonymousSignature:


               AnonymousSignature
                        ::= GeneralType IW? ParamTuple

referenced by:

AnonymousDeclaration
VariableType

ParamTuple:


               ParamTuple
                        ::= '(' IW? ParamList? IW? ')'

referenced by:

AnonymousSignature
Signature

ParamList:


               ParamList
                        ::= '/' ArgumentIdentifier IW? ',' IW? '/' ArgumentIdentifier
                          | VariableDeclarationList

referenced by:

ParamTuple

VariableDeclarationList:


               VariableDeclarationList
                        ::= VariableDeclaration ( IW? ',' IW? VariableDeclaration )*

referenced by:

ParamList

TypeWithCoord:


               TypeWithCoord
                        ::= Type LeftBound IW? ( RangeInSignature | CoordInSignature ) IW? RightBound

referenced by:

GeneralType

EntityWithCoord:


               EntityWithCoord
                        ::= Entity '[' IW? ( Range | CoordList ) IW? ']'

referenced by:

Assignee

CoordList:


               CoordList
                        ::= Coord ( IW? ',' IW? Coord )*

referenced by:

EntityWithCoord

CoordInSignature:


               CoordInSignature
                        ::= VariableType
                          | Coord

referenced by:

RangeInSignature
TypeWithCoord

Entity:


               Entity   ::= Variable
                          | AtList? 'self'

referenced by:

Assignee
EntityWithCoord

AtList:


               AtList   ::= '@'+

referenced by:

Entity

Coord:


               Coord    ::= Assignee
                          | PrimePredicate

referenced by:

CoordInSignature
CoordList
Range

RangeInSignature:


               RangeInSignature
                        ::= CoordInSignature? IW? '~' IW? CoordInSignature?

referenced by:

TypeWithCoord

Range:


               Range    ::= Coord? IW? '~' IW? Coord?

referenced by:

ClosedOrOpenRange
EntityWithCoord

CallModifier:


               CallModifier
                        ::= '*'
                          | '+'

referenced by:

GeneralType

ConditionFollowedByResultList:


               ConditionFollowedByResultList
                        ::= ConditionFollowedByResult ( CW* ConditionFollowedByResult )*

referenced by:

CaseStatement

ConditionFollowedByResult:


               ConditionFollowedByResult
                        ::= Predicate CW* ':' CW* StatementList

referenced by:

ConditionFollowedByResultList

TheoremLikeStatementOrConjecture:


               TheoremLikeStatementOrConjecture
                        ::= TheoremLikeStatementOrConjectureHeader SW Signature IW? PremiseConclusionBlock

referenced by:

BuildingBlock

TheoremLikeStatementOrConjectureHeader:


               TheoremLikeStatementOrConjectureHeader
                        ::= 'theorem'
                          | 'thm'
                          | 'conjecture'
                          | 'conj'
                          | 'proposition'
                          | 'prop'
                          | 'lemma'
                          | 'lem'
                          | 'corollary'
                          | 'cor'

referenced by:

TheoremLikeStatementOrConjecture

Proof:


               Proof    ::= ProofHeadHeader SW ProofIdentifier IW? ProofBlock

referenced by:

BuildingBlock

ProofIdentifier:


               ProofIdentifier
                        ::= PredicateIdentifier '' Digit

referenced by:

Proof

ProofHeadHeader:


               ProofHeadHeader
                        ::= 'proof'
                          | 'prf'

referenced by:

Proof

ProofBlock:


               ProofBlock
                        ::= '{' CW* VariableSpecificationList? CW* ProofArgumentList CW* '}'

referenced by:

Proof

ProofArgumentList:


               ProofArgumentList
                        ::= ProofArgument ( CW* ProofArgument )*

referenced by:

ProofBlock

ProofArgument:


               ProofArgument
                        ::= ArgumentIdentifier '.' SW ( Justification SW )? ArgumentInference SW

referenced by:

ProofArgumentList

AssumeHeader:


               AssumeHeader
                        ::= 'assume'
                          | 'ass'

referenced by:

AssumedPredicate

AssumedPredicate:


               AssumedPredicate
                        ::= AssumeHeader SW PremiseOrOtherPredicate

referenced by:

ArgumentInference

DerivedPredicate:


               DerivedPredicate
                        ::= '|-' SW ( Predicate | 'qed' | 'trivial' )

referenced by:

ArgumentInference
PremiseOrOtherPredicate

PremiseOrOtherPredicate:


               PremiseOrOtherPredicate
                        ::= PremiseHeader
                          | DerivedPredicate

referenced by:

AssumedPredicate

ArgumentInference:


               ArgumentInference
                        ::= AssumedPredicate
                          | DerivedPredicate
                          | Revoke

referenced by:

ProofArgument

Revoke:


               Revoke   ::= RevokeHeader SW '/' ArgumentIdentifier

referenced by:

ArgumentInference

RevokeHeader:


               RevokeHeader
                        ::= 'revoke'
                          | 'rev'

referenced by:

Revoke

Justification:


               Justification
                        ::= '/' ReferencedResultIdentifier ( IW? ',' IW? '/' ReferencedResultIdentifier )*

referenced by:

ProofArgument

ReferencedResultIdentifier:


               ReferencedResultIdentifier
                        ::= ArgumentIdentifier
                          | Signature
                          | PredicateIdentifier

referenced by:

Justification

Predicate:


               Predicate
                        ::= CompoundPredicate
                          | PrimePredicate

referenced by:

AssertionStatement
AssignmentStatement
AxiomBlock
ConclusionBlock
ConditionFollowedByResult
DerivedPredicate
Equivalence
ExclusiveOr
Implication
Localization
ParenthesisedPredicate
PredicateDefinitionBlock
PredicateList
PremiseBlock
ReturnStatement

PrimePredicate:


               PrimePredicate
                        ::= PredicateWithArguments
                          | QualifiedIdentifier
                          | Statement
                          | Identifier
                          | IsOperator
                          | 'true'
                          | 'false'
                          | UndefinedHeader

referenced by:

Coord
Predicate

QualifiedIdentifier:


               QualifiedIdentifier
                        ::= Identifier ( '.' PredicateWithArguments )+

referenced by:

PrimePredicate

PredicateWithArguments:


               PredicateWithArguments
                        ::= Identifier IW? '(' IW? PredicateList? IW? ')'

referenced by:

PrimePredicate
QualifiedIdentifier

Identifier:


               Identifier
                        ::= PredicateIdentifier
                          | AmpersandVariable
                          | IndexValue
                          | Assignee
                          | extDigit

referenced by:

IsOperator
PredicateWithArguments
PrimePredicate
QualifiedIdentifier

AmpersandVariable:


               AmpersandVariable
                        ::= '&' Variable

referenced by:

Identifier

IndexValue:


               IndexValue
                        ::= Variable '' ( Digit | Variable )

referenced by:

Identifier

PredicateList:


               PredicateList
                        ::= Predicate ( CW* ',' CW* Predicate )*

referenced by:

Conjunction
Disjunction
PredicateWithArguments

CompoundPredicate:


               CompoundPredicate
                        ::= Conjunction
                          | Disjunction
                          | Implication
                          | Equivalence
                          | ExclusiveOr
                          | Negation
                          | All
                          | Exists

referenced by:

Predicate

IsOperator:


               IsOperator
                        ::= 'is' IW? '(' CW* Identifier CW* ',' IW? VariableType IW? ')'

referenced by:

PrimePredicate

Negation:


               Negation ::= 'not' IW? ParenthesisedPredicate

referenced by:

CompoundPredicate

Conjunction:


               Conjunction
                        ::= 'and' CW* '(' CW* PredicateList CW* ')'

referenced by:

CompoundPredicate

Disjunction:


               Disjunction
                        ::= 'or' CW* '(' CW* PredicateList CW* ')'

referenced by:

CompoundPredicate

Implication:


               Implication
                        ::= 'impl' CW? '(' CW* Predicate CW* ',' CW* Predicate CW* ')'

referenced by:

CompoundPredicate

Equivalence:


               Equivalence
                        ::= 'iif' CW? '(' CW* Predicate CW* ',' CW* Predicate CW* ')'

referenced by:

CompoundPredicate

ExclusiveOr:


               ExclusiveOr
                        ::= 'xor' CW? '(' CW* Predicate CW* ',' CW* Predicate CW* ')'

referenced by:

CompoundPredicate

ParenthesisedPredicate:


               ParenthesisedPredicate
                        ::= '(' CW* Predicate CW* ')'

referenced by:

All
Exists
Negation

All:


               All      ::= 'all' SW VariableList CW? ParenthesisedPredicate

referenced by:

CompoundPredicate

Exists:


               Exists   ::= ExistsHeader SW VariableList CW? ParenthesisedPredicate

referenced by:

CompoundPredicate

ExistsHeader:


               ExistsHeader
                        ::= ExistsTimesN
                          | 'ex'

referenced by:

Exists

ExistsTimesN:


               ExistsTimesN
                        ::= 'ex' '' Digit

referenced by:

ExistsHeader

PythonDelegate:


               PythonDelegate
                        ::= 'py' '.' PythonIdentifier IW? '(' IW? VariableList IW? ')'

referenced by:

Statement

PythonIdentifier:


               PythonIdentifier
                        ::= regular_expression '/[a-z_]+/'

referenced by:

PythonDelegate

StatementList:


               StatementList
                        ::= Statement SW ( CW* Statement SW )*

referenced by:

ConditionFollowedByResult
DefaultResult
RangeOrLoopBody

Statement:


               Statement
                        ::= PythonDelegate
                          | CaseStatement
                          | AssertionStatement
                          | AssignmentStatement
                          | RangeStatement
                          | LoopStatement
                          | ReturnStatement

referenced by:

PrimePredicate
StatementList
VariableSpecification

ReturnStatement:


               ReturnStatement
                        ::= ReturnHeader SW Predicate

referenced by:

Statement

CaseStatement:


               CaseStatement
                        ::= 'case' CW* '(' CW* ConditionFollowedByResultList CW* DefaultResult CW* ')'

referenced by:

Statement

LoopStatement:


               LoopStatement
                        ::= 'loop' SW RangeOrLoopBody

referenced by:

Statement

RangeStatement:


               RangeStatement
                        ::= 'range' SW RangeOrLoopBody

referenced by:

Statement

RangeOrLoopBody:


               RangeOrLoopBody
                        ::= Assignee SW ( KeysOfVariadicVariable | ClosedOrOpenRange | Assignee ) CW* '(' CW* StatementList CW* ')'

referenced by:

LoopStatement
RangeStatement

KeysOfVariadicVariable:


               KeysOfVariadicVariable
                        ::= Variable ''

referenced by:

RangeOrLoopBody

ClosedOrOpenRange:


               ClosedOrOpenRange
                        ::= LeftBound IW? Range IW? RightBound

referenced by:

RangeOrLoopBody

LeftBound:


               LeftBound
                        ::= '[' '!'?

referenced by:

ClosedOrOpenRange
TypeWithCoord

RightBound:


               RightBound
                        ::= '!'? ']'

referenced by:

ClosedOrOpenRange
TypeWithCoord

DefaultResult:


               DefaultResult
                        ::= 'else' IW? ':' CW* StatementList

referenced by:

CaseStatement

AssignmentStatement:


               AssignmentStatement
                        ::= Assignee IW? ':=' IW? Predicate

referenced by:

Statement

Assignee:


               Assignee ::= EntityWithCoord
                          | Entity

referenced by:

AssignmentStatement
Coord
Identifier
RangeOrLoopBody

ReturnHeader:


               ReturnHeader
                        ::= 'return'
                          | 'ret'

referenced by:

ReturnStatement

UndefinedHeader:


               UndefinedHeader
                        ::= 'undefined'
                          | 'undef'

referenced by:

PrimePredicate

NamespaceIdentifier:


               NamespaceIdentifier
                        ::= IdStartsWithCap ( '.' IdStartsWithCap )*

referenced by:

Namespace
WildcardTheoryNamespace

ArgumentIdentifier:


               ArgumentIdentifier
                        ::= Digit IdStartsWithSmallCase?

referenced by:

ParamList
ProofArgument
ReferencedResultIdentifier
Revoke

WildcardTheoryNamespace:


               WildcardTheoryNamespace
                        ::= NamespaceIdentifier NamespaceModifier?

referenced by:

WildcardTheoryNamespaceList

NamespaceModifier:


               NamespaceModifier
                        ::= '.' '*'
                          | Alias

referenced by:

WildcardTheoryNamespace

Alias:


               Alias    ::= IW 'alias' IW IdStartsWithCap

referenced by:

NamespaceModifier

IdStartsWithCap:


               IdStartsWithCap
                        ::= regular_expression '/[A-Z][a-z0-9A-Z_]*/'

referenced by:

Alias
AliasedId
LongTemplateHeader
NamespaceIdentifier
PredicateIdentifier
XId

IdStartsWithSmallCase:


               IdStartsWithSmallCase
                        ::= regular_expression '/[a-z][a-z0-9A-Z_]*/'

referenced by:

ArgumentIdentifier
Variable

SW:


               SW       ::= IW

referenced by:

All
AssertionStatement
AssumedPredicate
Axiom
ClassInstance
DefinitionClass
DefinitionPredicate
DerivedPredicate
Exists
ExtensionBlock
ExtensionTail
FunctionalTermSignature
LoopStatement
Proof
ProofArgument
Property
RangeOrLoopBody
RangeStatement
ReturnStatement
Revoke
StatementList
TheoremLikeStatementOrConjecture
TranslationList
UsesClause
VariableSpecificationList

CW:


               CW       ::= IW
                          | Comment
                          | LongComment

referenced by:

All
Axiom
AxiomBlock
BuildingBlockList
CaseStatement
ClassInstance
ConclusionBlock
ConditionFollowedByResult
ConditionFollowedByResultList
Conjunction
Constructor
DefaultResult
DefinitionClass
DefinitionContentList
DefinitionFunctionalTerm
DefinitionPredicate
Disjunction
Equivalence
ExclusiveOr
Exists
FunctionalTermDefinitionBlock
FunctionalTermInstance
Implication
InstanceBlock
IsOperator
LocalizationBlock
LocalizationList
Namespace
NamespaceBlock
ObjectDefinitionBlock
ParenthesisedPredicate
PredicateDefinitionBlock
PredicateList
PremiseBlock
PremiseConclusionBlock
ProofArgumentList
ProofBlock
Property
RangeOrLoopBody
RuleOfInferenceList
RulesOfInferenceBlock
StatementList
TheoryBlock
VariableSpecificationList

Comment:


               Comment  ::= regular_expression '/\/\/[^\n]*/'

referenced by:

LongComment:


               LongComment
                        ::= regular_expression '/\/\*((?:.|\n)*?)\*\//'

referenced by:

IW:


               IW       ::= regular_expression '/(\r\n\t]+/'

referenced by:

Alias
AnonymousSignature
AssignmentStatement
CW
ClosedOrOpenRange
ConclusionBlock
CoordList
DefaultResult
DefinitionClass
EBNFFactor
EBNFTerm
EBNFTransl
EntityWithCoord
ExtensionBlock
FunctionalTermSignature
IsOperator
Justification
Localization
Mapping
NamedVariableDeclaration
Negation
ParamList
ParamTuple
PredicateWithArguments
PremiseBlock
Proof
PythonDelegate
Range
RangeInSignature
RuleOfInference
SW
Signature
TheoremLikeStatementOrConjecture
Translation
TupleOfTypes
TypeWithCoord
VariableDeclarationList
VariableList
WildcardTheoryNamespaceList

XId:


               XId      ::= '@' 'ext' IdStartsWithCap

referenced by:

Type

Variable:


               Variable ::= IdStartsWithSmallCase

referenced by:

AmpersandVariable
EBNFFactor
Entity
IndexValue
KeysOfVariadicVariable
VariableList

Digit:


               Digit    ::= regular_expression '/\d+/'

referenced by:

ArgumentIdentifier
ExistsTimesN
IndexValue
LongTemplateHeader
ProofIdentifier

LocalizationBlock:


               LocalizationBlock
                        ::= LocalizationHeader CW* '{' CW* LocalizationList CW* '}'

referenced by:

NamespaceBlock

LocalizationList:


               LocalizationList
                        ::= Localization ( CW* Localization )*

referenced by:

LocalizationBlock

Localization:


               Localization
                        ::= Predicate IW? ':=' IW? TranslationList IW? ';'

referenced by:

LocalizationList

TranslationList:


               TranslationList
                        ::= Translation ( SW Translation )*

referenced by:

Localization

Translation:


               Translation
                        ::= '~' LanguageCode IW? ':' IW? EBNFTransl

referenced by:

TranslationList

LanguageCode:


               LanguageCode
                        ::= regular_expression '/[a-z]{3}/'

referenced by:

Translation

EBNFTransl:


               EBNFTransl
                        ::= EBNFTerm ( IW? '|' IW? EBNFTerm )*

referenced by:

EBNFFactor
Translation

EBNFTerm:


               EBNFTerm ::= EBNFFactor ( IW? EBNFFactor )*

referenced by:

EBNFTransl

EBNFFactor:


               EBNFFactor
                        ::= Variable
                          | EBNFString
                          | '(' IW? EBNFTransl IW? ')'

referenced by:

EBNFTerm

EBNFString:


               EBNFString
                        ::= regular_expression '/\"[^\"]*\"/'

referenced by:

EBNFFactor

LocalizationHeader:


               LocalizationHeader
                        ::= 'localization'
                          | 'loc'

referenced by:

LocalizationBlock

extDigit:


               extDigit ::= regular_expression '/\d+/'

referenced by:

Identifier

... generated by RR - Railroad Diagram Generator