blob: b9a2013c92f99ef3abd958e5873d613667469e26 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
--# -path=present
concrete LogicCnc of Logic = {
lincat
Ind = {s : Str};
Prop = {s:Str};
lin
john = {s="john"};
mary = {s="mary"};
boy x = {s="boy"++"("++x.s++")"};
smart x = {s="smart"++"("++x.s++")"};
love x y = {s="love"++"("++x.s++","++y.s++")"};
leave x = {s="leave"++"("++x.s++")"};
and x y = {s=x.s++"&&"++y.s};
or x y = {s=x.s++"||"++y.s};
impl x y = {s=x.s++"=>"++y.s};
forall f = {s="forall"++f.$0++"."++"("++f.s++")"};
exists f = {s="exists"++f.$0++"."++"("++f.s++")"};
not p = {s="not"++"("++p.s++")"};
eq x y = {s=x.s++"="++y.s};
}
|