blob: 0b5f6957e156fc73ff7572effc2cbf7787fe3926 (
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
52
53
54
55
56
57
58
59
|
-- File name System/specific.Abs.gf
abstract specSystem = specific, genSystem ** {
cat
StartTimeQ ;
EndTimeQ ;
ChToStoreQ ;
WdToStoreQ ;
fun
confirmRecJob : Action -> DMove;
---- vcr_add_rec_job_no_args : Action ; -- spela in! moved to specific
q_lambdaActionDel : DelAction -> WHQuestion ;
-- Time in question
startTimeToStoreQ : Time -> StartTimeQ ;
endTimeToStoreQ : Time -> EndTimeQ ;
--- Channel and Weekday in question
channelToStoreQ : Channel -> ChToStoreQ ;
weekdayToStoreQ : Weekday -> WdToStoreQ ;
--- WHQuestions --- Lambdas
q_lambdaStartTime : StartTime -> WHQuestion ;
q_lambdaEndTime : EndTime -> WHQuestion ;
q_lambdaWeekday : WdToStore -> WHQuestion ;
q_lambdaChannel : ChToStore -> WHQuestion ;
--- Constructions for ynquestions
ynQuST : StartTimeQ -> YNQuestion ;
ynQuET : EndTimeQ -> YNQuestion ;
ynQuCH : ChToStoreQ -> YNQuestion ;
ynQuWD: WdToStoreQ -> YNQuestion ;
--- Props
startTimeToStoreProp : StartTime -> Prop ;
endTimeToStoreProp : EndTime -> Prop ;
channelToStoreProp : ChToStore -> Prop ;
weekdayToStoreProp : WdToStore -> Prop ;
cat
ChannelList ;
Channels ;
ChannelAction ;
fun
channelListing : Channels -> ChannelList ;
channels1 : Channel -> Channels ;
channels2 : Channel -> Channels -> Channel ;
channelListAction : ChannelList -> ChannelAction ;
--channelListAction : ChannelList -> DMove ;
channelListActionDMove : ChannelAction -> DMove ;
}
|
