mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-09 13:09:33 -06:00
42 lines
839 B
Plaintext
42 lines
839 B
Plaintext
abstract Math = {
|
|
|
|
flags startcat = Section ;
|
|
|
|
cat
|
|
Section ; Label ; Context ; Typ ; Obj ; Prop ; Proof ; Var ;
|
|
|
|
fun
|
|
SDefObj : Label -> Context -> Obj -> Typ -> Obj -> Section ;
|
|
SDefProp : Label -> Context -> Prop -> Prop -> Section ;
|
|
SAxiom : Label -> Context -> Prop -> Section ;
|
|
STheorem : Label -> Context -> Prop -> Proof -> Section ;
|
|
|
|
CEmpty : Context ;
|
|
CObj : Var -> Typ -> Context -> Context ;
|
|
CProp : Prop -> Context -> Context ;
|
|
|
|
OVar : Var -> Obj ;
|
|
|
|
LNone : Label ;
|
|
LString : String -> Label ;
|
|
VString : String -> Var ;
|
|
|
|
V_x, V_y, V_z : Var ; --- for js
|
|
|
|
PLink : Proof ;
|
|
|
|
-- lexicon
|
|
|
|
Set : Typ ;
|
|
Nat : Typ ;
|
|
Zero : Obj ;
|
|
Succ : Obj -> Obj ;
|
|
One : Obj ;
|
|
Two : Obj ;
|
|
Even : Obj -> Prop ;
|
|
Odd : Obj -> Prop ;
|
|
Prime : Obj -> Prop ;
|
|
Divisible : Obj -> Obj -> Prop ;
|
|
|
|
}
|