mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-09 04:59:31 -06:00
46 lines
960 B
Plaintext
46 lines
960 B
Plaintext
abstract MathText = Logic ** {
|
|
|
|
flags startcat = Book ;
|
|
|
|
cat
|
|
Book ;
|
|
Section ;
|
|
[Section] {1} ;
|
|
Paragraph ;
|
|
[Paragraph] {1} ;
|
|
Statement ;
|
|
Declaration ;
|
|
[Declaration] {0} ;
|
|
Ident ;
|
|
Proof ;
|
|
Case ;
|
|
[Case] {2} ;
|
|
Number ;
|
|
|
|
fun
|
|
MkBook : [Section] -> Book ;
|
|
|
|
ParAxiom : Ident -> Statement -> Section ;
|
|
ParTheorem : Ident -> Statement -> Proof -> Section ;
|
|
|
|
ParDefInd : [Declaration] -> Ind -> Ind -> Section ;
|
|
ParDefPred1 : [Declaration] -> Ind -> Pred1 -> Prop -> Section ;
|
|
ParDefPred2 : [Declaration] -> Ind -> Pred2 -> Ind -> Prop -> Section ;
|
|
|
|
StProp : [Declaration] -> Prop -> Statement ;
|
|
|
|
DecVar : [Var] -> Dom -> Declaration ;
|
|
DecProp : Prop -> Declaration ;
|
|
|
|
PrEnd : Proof ;
|
|
PrStep : Statement -> Proof -> Proof ;
|
|
PrBy : Ident -> Prop -> Proof -> Proof ;
|
|
PrCase : Number -> [Case] -> Proof ;
|
|
CProof : Ident -> Proof -> Case ;
|
|
|
|
IdStr : String -> Ident ;
|
|
|
|
Two, Three, Four, Five : Number ;
|
|
|
|
}
|