FPL Syntax Diagrams (Version 1.1.3)

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? Type 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? VariableType

referenced by:

FunctionalTermSignature

VariableSpecificationList:


               VariableSpecificationList
                        ::= ( CW* VariableSpecification SW )+

referenced by:

AxiomBlock
FunctionalTermDefinitionBlock
InstanceBlock
ObjectDefinitionBlock
PredicateDefinitionBlock
PredicateInstanceBlock
PremiseConclusionBlock
ProofBlock

VariableSpecification:


               VariableSpecification
                        ::= Statement
                          | NamedVariableDeclaration

referenced by:

VariableSpecificationList

AssertionStatement:


               AssertionStatement
                        ::= 'assert' SW Predicate

referenced by:

Statement

NamedVariableDeclaration:


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

referenced by:

NamedVariableDeclarationList
VariableSpecification

VariableType:


               VariableType
                        ::= ParenthesisedGeneralType
                          | GeneralType

referenced by:

ClassInstance
Mapping
NamedVariableDeclaration

GeneralType:


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

referenced by:

IsOperator
ParenthesisedGeneralType
VariableType

IndexHeader:


               IndexHeader
                        ::= 'index'
                          | 'ind'

referenced by:

GeneralType

Type:


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

referenced by:

DefinitionClass
GeneralType
TypeWithCoord

VariableList:


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

referenced by:

All
Exists
NamedVariableDeclaration

DefinitionPredicate:


               DefinitionPredicate
                        ::= PredicateHeader SW Signature CW* PredicateDefinitionBlock

referenced by:

Definition

PredicateHeader:


               PredicateHeader
                        ::= 'predicate'
                          | 'pred'

referenced by:

DefinitionPredicate
PredicateInstance
Type

FunctionalTermHeader:


               FunctionalTermHeader
                        ::= 'function'
                          | 'func'

referenced by:

FunctionalTermSignature
Type

PredicateDefinitionBlock:


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

referenced by:

DefinitionPredicate

PredicateInstanceBlock:


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

referenced by:

PredicateInstance

PredicateIdentifier:


               PredicateIdentifier
                        ::= AliasedId
                          | IdStartsWithCap

referenced by:

DefinitionClass
Identifier
ReferencingIdentifier
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
PredicateDefinitionBlock

Property:


               Property ::= CW* PropertyHeader SW DefinitionProperty

referenced by:

DefinitionContent
PropertyList

DefinitionProperty:


               DefinitionProperty
                        ::= PredicateInstance
                          | FunctionalTermInstance
                          | ClassInstance

referenced by:

Property

ClassInstance:


               ClassInstance
                        ::= VariableType SW Signature CW* InstanceBlock

referenced by:

DefinitionProperty

FunctionalTermInstance:


               FunctionalTermInstance
                        ::= FunctionalTermSignature CW* InstanceBlock

referenced by:

DefinitionProperty

PredicateInstance:


               PredicateInstance
                        ::= PredicateHeader SW Signature CW* PredicateInstanceBlock

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
PredicateInstance
RuleOfInference
TheoremLikeStatementOrConjecture

ParenthesisedGeneralType:


               ParenthesisedGeneralType
                        ::= GeneralType IW? ParamTuple

referenced by:

VariableType

ParamTuple:


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

referenced by:

CorollarySignature
ParenthesisedGeneralType
Signature

ArgumentParam:


               ArgumentParam
                        ::= '/' ArgumentIdentifier

referenced by:

PrimePredicate
Revoke

NamedVariableDeclarationList:


               NamedVariableDeclarationList
                        ::= NamedVariableDeclaration ( IW? ',' IW? NamedVariableDeclaration )*

referenced by:

ParamTuple

TypeWithCoord:


               TypeWithCoord
                        ::= Type LeftBound IW? ( RangeInType | CoordInType ) IW? RightBound

referenced by:

GeneralType

RangeInType:


               RangeInType
                        ::= CoordInType? IW? '~' IW? CoordInType?

referenced by:

TypeWithCoord

CoordInType:


               CoordInType
                        ::= PredicateWithArguments
                          | Variable

referenced by:

RangeInType
TypeWithCoord

EntityWithCoord:


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

referenced by:

Assignee

CoordList:


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

referenced by:

EntityWithCoord

Entity:


               Entity   ::= Variable
                          | AtList? 'self'

referenced by:

Assignee
EntityWithCoord

AtList:


               AtList   ::= '@'+

referenced by:

Entity

Coord:


               Coord    ::= Assignee
                          | PrimePredicate

referenced by:

CoordList
Range

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 ( CorollarySignature | Signature ) IW? PremiseConclusionBlock

referenced by:

BuildingBlock

TheoremLikeStatementOrConjectureHeader:


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

referenced by:

TheoremLikeStatementOrConjecture

CorollarySignature:


               CorollarySignature
                        ::= ReferencingIdentifier IW? ParamTuple

referenced by:

TheoremLikeStatementOrConjecture

CorollaryHeader:


               CorollaryHeader
                        ::= 'corollary'
                          | 'cor'

referenced by:

TheoremLikeStatementOrConjectureHeader

Proof:


               Proof    ::= ProofHeader SW ReferencingIdentifier IW? ProofBlock

referenced by:

BuildingBlock

ReferencingIdentifier:


               ReferencingIdentifier
                        ::= PredicateIdentifier DollarDigitList

referenced by:

CorollarySignature
Proof

DollarDigitList:


               DollarDigitList
                        ::= ( '' Digit )+

referenced by:

ReferencingIdentifier

ProofHeader:


               ProofHeader
                        ::= '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
                        ::= PremiseHeader
                          | Predicate

referenced by:

AssumedPredicate

ArgumentInference:


               ArgumentInference
                        ::= AssumedPredicate
                          | DerivedPredicate
                          | Revoke

referenced by:

ProofArgument

Revoke:


               Revoke   ::= RevokeHeader SW ArgumentParam

referenced by:

ArgumentInference

RevokeHeader:


               RevokeHeader
                        ::= 'revoke'
                          | 'rev'

referenced by:

Revoke

Justification:


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

referenced by:

ProofArgument

Predicate:


               Predicate
                        ::= CompoundPredicate
                          | PrimePredicate

referenced by:

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

PrimePredicate:


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

referenced by:

Coord
Justification
Predicate

QualifiedIdentifier:


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

referenced by:

PrimePredicate

PredicateWithArguments:


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

referenced by:

CoordInType
PrimePredicate
QualifiedIdentifier

Identifier:


               Identifier
                        ::= PredicateIdentifier
                          | IndexValue
                          | Assignee

referenced by:

IsOperator
PredicateWithArguments
PrimePredicate
QualifiedIdentifier

IndexValue:


               IndexValue
                        ::= KeysOfVariadicVariable ( Digit | Variable )

referenced by:

Identifier

PredicateList:


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

referenced by:

Conjunction
Disjunction
PredicateWithArguments
PythonDelegate

CompoundPredicate:


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

referenced by:

Predicate

IsOperator:


               IsOperator
                        ::= 'is' IW? '(' CW* Identifier CW* ',' IW? GeneralType 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? PredicateList 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 VariableRange CW* '(' CW* StatementList CW* ')'

referenced by:

LoopStatement
RangeStatement

VariableRange:


               VariableRange
                        ::= KeysOfVariadicVariable
                          | ClosedOrOpenRange
                          | Assignee

referenced by:

RangeOrLoopBody

KeysOfVariadicVariable:


               KeysOfVariadicVariable
                        ::= Variable ''

referenced by:

IndexValue
VariableRange

ClosedOrOpenRange:


               ClosedOrOpenRange
                        ::= LeftBound IW? Range IW? RightBound

referenced by:

VariableRange

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
VariableRange

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:

ArgumentParam
ProofArgument

WildcardTheoryNamespace:


               WildcardTheoryNamespace
                        ::= NamespaceIdentifier NamespaceModifier?

referenced by:

WildcardTheoryNamespaceList

NamespaceModifier:


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

referenced by:

WildcardTheoryNamespace

Alias:


               Alias    ::= SW 'alias' SW 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:

Alias
All
AssertionStatement
AssumedPredicate
Axiom
ClassInstance
DefinitionClass
DefinitionPredicate
DerivedPredicate
Exists
ExtensionBlock
ExtensionTail
FunctionalTermSignature
LoopStatement
PredicateInstance
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
PredicateInstance
PredicateInstanceBlock
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:

AssignmentStatement
CW
ClosedOrOpenRange
ConclusionBlock
CoordList
CorollarySignature
DefaultResult
DefinitionClass
EBNFFactor
EBNFTerm
EBNFTransl
EntityWithCoord
ExtensionBlock
FunctionalTermSignature
IsOperator
Justification
Localization
Mapping
NamedVariableDeclaration
NamedVariableDeclarationList
Negation
ParamTuple
ParenthesisedGeneralType
PredicateWithArguments
PremiseBlock
Proof
PythonDelegate
Range
RangeInType
RuleOfInference
SW
Signature
TheoremLikeStatementOrConjecture
Translation
TypeWithCoord
VariableList
WildcardTheoryNamespaceList

XId:


               XId      ::= '@' 'ext' IdStartsWithCap

referenced by:

Type

Variable:


               Variable ::= IdStartsWithSmallCase

referenced by:

CoordInType
EBNFFactor
Entity
IndexValue
KeysOfVariadicVariable
VariableList

Digit:


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

referenced by:

ArgumentIdentifier
DollarDigitList
ExistsTimesN
IndexValue
LongTemplateHeader

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:

PrimePredicate

... generated by RR - Railroad Diagram Generator