blob: 848b583aabe6fa59d909261a3bb8797a2d75bdb4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
|
incomplete concrete MathI of Math = open
Syntax,
Mathematical,
LexMath,
Prelude in {
lincat
Prop = S ;
Exp = NP ;
lin
And = mkS and_Conj ;
Or = mkS or_Conj ;
If a = mkS (mkAdv if_Subj a) ;
Zero = mkNP zero_PN ;
Successor = funct1 successor_N2 ;
Sum = funct2 sum_N2 ;
Product = funct2 product_N2 ;
Even = pred1 even_A ;
Odd = pred1 odd_A ;
Prime = pred1 prime_A ;
Equal = pred2 equal_A2 ;
Less = predC small_A ;
Greater = predC great_A ;
Divisible = pred2 divisible_A2 ;
oper
funct1 : N2 -> NP -> NP = \f,x -> mkNP the_Art (mkCN f x) ;
funct2 : N2 -> NP -> NP -> NP = \f,x,y -> mkNP the_Art (mkCN f (mkNP and_Conj x y)) ;
pred1 : A -> NP -> S = \f,x -> mkS (mkCl x f) ;
pred2 : A2 -> NP -> NP -> S = \f,x,y -> mkS (mkCl x f y) ;
predC : A -> NP -> NP -> S = \f,x,y -> mkS (mkCl x f y) ;
lincat
Var = Symb ;
lin
X = MkSymb (ss "x") ;
Y = MkSymb (ss "y") ;
EVar x = mkNP (SymbPN x) ;
EInt i = mkNP (IntPN i) ;
ANumberVar x = mkNP a_Art (mkCN (mkCN number_N) (mkNP (SymbPN x))) ;
TheNumberVar x = mkNP the_Art (mkCN (mkCN number_N) (mkNP (SymbPN x))) ;
}
|
