blob: 31163cffed4f68d3ef9edd9cfbf3216c259f37a1 (
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
|
abstract Dialogue = {
flags startcat=Move ;
cat
Move ;
Action ;
Proposition ;
Question ;
Kind ;
Object Kind ;
Oper0 ;
Oper1 Kind ;
Oper2 Kind Kind ;
fun
MRequest : Action -> Move ;
MConfirm : Action -> Move ;
MAnswer : Proposition -> Move ;
MIssue : Question -> Move ;
MYes : Move ;
MNo : Move ;
MObject : (k : Kind) -> Object k -> Move ;
PAction : Action -> Proposition ;
QKind : Kind -> Question ;
AOper0 : Oper0 -> Action ;
AOper1 : (k : Kind) -> Oper1 k -> Object k -> Action ;
AOper2 : (k,m : Kind) -> Oper2 k m -> Object k -> Object m -> Action ;
OAll : (k : Kind) -> Object k ;
OIndef : (k : Kind) -> Object k ;
ODef : (k : Kind) -> Object k ;
}
|