Files
gf-core/gf-book/examples/chapter9/Anaphora.gf
2011-01-11 15:46:43 +00:00

18 lines
417 B
Plaintext

abstract Anaphora = TestSemantics - [she_NP] ** {
cat
Proof Prop ;
fun
IfS : (A : S) -> (Proof (iS A) -> S) -> S ;
AnaNP : (A : CN) -> (a : Ind) -> Proof (iCN A a) -> NP ;
pe : (B : Ind -> Prop) -> Proof (Exist B) -> Ind ;
qe : (B : Ind -> Prop) -> (c : Proof (Exist B)) -> Proof (B (pe B c)) ;
pc : (A,B : Prop) -> Proof (And A B) -> Proof A ;
qc : (A,B : Prop) -> Proof (And A B) -> Proof B ;
}