forked from GitHub/gf-core
75 lines
2.0 KiB
Plaintext
75 lines
2.0 KiB
Plaintext
incomplete concrete MathTextI of MathText = Logic **
|
|
open
|
|
Syntax,
|
|
(Lang = Lang), ---- for ImpP3, SSubjS
|
|
Symbolic,
|
|
LexLogic in {
|
|
|
|
lincat
|
|
Book = Text ;
|
|
Section = Text ;
|
|
[Section] = Text ;
|
|
Paragraph = Text ;
|
|
[Paragraph] = Text ;
|
|
Statement = Text ;
|
|
Declaration = Utt ;
|
|
[Declaration] = Text ;
|
|
Ident = NP ;
|
|
Proof = Text ;
|
|
Case = Text ;
|
|
[Case] = Text ;
|
|
Number = Card ;
|
|
|
|
lin
|
|
MkBook ss = ss ;
|
|
|
|
ParAxiom id stm = mkText (mkText (Lang.UttCN (mkCN axiom_N id))) stm ;
|
|
ParTheorem id stm pr =
|
|
mkText (mkText (mkText (Lang.UttCN (mkCN theorem_N id))) stm) pr ;
|
|
|
|
ParDefInd cont dum dens =
|
|
definition (mkText cont (mkText (mkCl (mkNP we_Pron) define_V3 dum dens))) ;
|
|
ParDefPred1 cont arg dum dens =
|
|
definition (mkText cont (mkText (Lang.SSubjS
|
|
(mkS (mkCl (mkNP we_Pron) define_V2V arg dum))
|
|
if_Subj dens))) ;
|
|
ParDefPred2 cont arg dum obj dens =
|
|
definition (mkText cont (mkText (Lang.SSubjS
|
|
(mkS (mkCl (mkNP we_Pron) define_V2V arg (mkVP dum obj)))
|
|
if_Subj dens))) ;
|
|
|
|
BaseSection s = s ;
|
|
ConsSection s ss = mkText s ss ;
|
|
BaseParagraph s = s ;
|
|
ConsParagraph s ss = mkText s ss ;
|
|
BaseCase s t = mkText s t ;
|
|
ConsCase s ss = mkText s ss ;
|
|
BaseDeclaration = emptyText ;
|
|
ConsDeclaration s ss = mkText (mkPhr s) ss ;
|
|
|
|
|
|
StProp ds prop = mkText ds (mkText prop) ;
|
|
|
|
DecVar xs dom =
|
|
Lang.ImpP3 xs.p1 (mkVP (indef xs.p2 (mkCN dom))) ;
|
|
-- mkUtt (mkImp (mkVP let_V2V xs.p1 (mkVP (indef xs.p2 (mkCN dom))))) ;
|
|
DecProp prop = mkUtt prop ;
|
|
|
|
PrEnd = emptyText ;
|
|
PrStep st pr = mkText st pr ;
|
|
PrBy id prop proof = mkText (mkText (mkS (mkAdv by_Prep id) prop)) proof ;
|
|
PrCase num cs =
|
|
mkText (mkPhr (mkCl (mkNP we_Pron) have_V2 (mkNP num case_N))) cs ;
|
|
CProof id proof = mkText (mkPhr (mkUtt (mkNP (mkCN case_N id)))) proof ;
|
|
|
|
IdStr s = symb s.s ;
|
|
|
|
Two = mkCard n2_Numeral ;
|
|
Three = mkCard n3_Numeral ;
|
|
Four = mkCard n4_Numeral ;
|
|
Five = mkCard n5_Numeral ;
|
|
|
|
oper
|
|
definition : Text -> Text = mkText (mkText (Lang.UttCN (mkCN definition_N))) ;
|
|
}
|