blob: 5cbb92c942c4f53d99fdce3802c67943941e62cd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
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 ;
}
|
