| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (308 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (113 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (129 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (23 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (29 entries) |
Global Index
A
aasp [constructor, in Copland.Term]aatt [constructor, in Copland.Term]
abpar [constructor, in Copland.Term]
abseq [constructor, in Copland.Term]
aeval [definition, in Copland.Term]
alseq [constructor, in Copland.Term]
anno [definition, in Copland.Term]
annotated [definition, in Copland.Term]
AnnoTerm [inductive, in Copland.Term]
anno_well_formed [lemma, in Copland.Term]
anno_range [lemma, in Copland.Term]
arg [constructor, in Copland.Term]
Arg [inductive, in Copland.Term]
asp [constructor, in Copland.Term]
ASP [inductive, in Copland.Term]
asp_event [definition, in Copland.Term]
att [constructor, in Copland.Term]
at_range [lemma, in Copland.Term]
B
before [constructor, in Copland.Event_system]before_sup [lemma, in Copland.Event_system]
before_associative_pairs [lemma, in Copland.Event_system]
before_associative [lemma, in Copland.Event_system]
bp [constructor, in Copland.LTS]
bpar [constructor, in Copland.Term]
bra_range [lemma, in Copland.Term]
bseq [constructor, in Copland.Term]
bsl [constructor, in Copland.LTS]
bsr [constructor, in Copland.LTS]
C
conf [constructor, in Copland.LTS]copy [constructor, in Copland.Term]
correct_path_exists [lemma, in Copland.LTS]
CPY [constructor, in Copland.Term]
D
disjoint_lists [definition, in Copland.More_lists]E
earlier [definition, in Copland.More_lists]earlier_cons_shift [lemma, in Copland.More_lists]
earlier_cons [lemma, in Copland.More_lists]
earlier_append_iff [lemma, in Copland.More_lists]
earlier_append [lemma, in Copland.More_lists]
earlier_right [lemma, in Copland.More_lists]
earlier_left [lemma, in Copland.More_lists]
earlier_in_right [lemma, in Copland.More_lists]
earlier_in_left [lemma, in Copland.More_lists]
ein_merger [constructor, in Copland.Event_system]
ein_mergel [constructor, in Copland.Event_system]
ein_beforer [constructor, in Copland.Event_system]
ein_beforel [constructor, in Copland.Event_system]
ein_leaf [constructor, in Copland.Event_system]
eq_ev_dec [definition, in Copland.Term]
eq_arg_dec [definition, in Copland.Term]
esize [definition, in Copland.Term]
esizeS [definition, in Copland.Main]
esizeS_tr [lemma, in Copland.Main]
esize_tr [lemma, in Copland.Main]
es_injective_events [lemma, in Copland.Event_system]
es_size [definition, in Copland.Event_system]
es_range [definition, in Copland.Event_system]
ES_Range [definition, in Copland.Event_system]
ev [definition, in Copland.Term]
Ev [inductive, in Copland.Term]
eval [definition, in Copland.Term]
eval_aeval [lemma, in Copland.Term]
eval_asp [definition, in Copland.Term]
events [inductive, in Copland.Term]
events_injective [lemma, in Copland.Term]
events_range_event [lemma, in Copland.Term]
events_range [lemma, in Copland.Term]
Event_system.ev [variable, in Copland.Event_system]
Event_system.A [variable, in Copland.Event_system]
Event_system [section, in Copland.Event_system]
Event_system [library]
Evidence [inductive, in Copland.Term]
EvSys [inductive, in Copland.Event_system]
evsys_max_unique [lemma, in Copland.Term_system]
evsys_events [lemma, in Copland.Term_system]
evsys_range [lemma, in Copland.Term_system]
evsys_transitive [lemma, in Copland.Event_system]
evsys_irreflexive [lemma, in Copland.Event_system]
evsys_tr_in [lemma, in Copland.Trace]
evtsatt [constructor, in Copland.Term]
evtsattreq [constructor, in Copland.Term]
evtsattrpy [constructor, in Copland.Term]
evtsbparjoin [constructor, in Copland.Term]
evtsbparl [constructor, in Copland.Term]
evtsbparr [constructor, in Copland.Term]
evtsbparsplit [constructor, in Copland.Term]
evtsbseqjoin [constructor, in Copland.Term]
evtsbseql [constructor, in Copland.Term]
evtsbseqr [constructor, in Copland.Term]
evtsbseqsplit [constructor, in Copland.Term]
evtscpy [constructor, in Copland.Term]
evtshsh [constructor, in Copland.Term]
evtskim [constructor, in Copland.Term]
evtslseql [constructor, in Copland.Term]
evtslseqr [constructor, in Copland.Term]
evtssig [constructor, in Copland.Term]
evtsusm [constructor, in Copland.Term]
ev_sys [definition, in Copland.Term_system]
ev_in [inductive, in Copland.Event_system]
F
firstn_in [lemma, in Copland.More_lists]firstn_all_n [lemma, in Copland.More_lists]
firstn_append [lemma, in Copland.More_lists]
G
gg [constructor, in Copland.Term]H
halt [definition, in Copland.LTS]halt_size [lemma, in Copland.LTS]
hash [constructor, in Copland.Term]
hh [constructor, in Copland.Term]
HSH [constructor, in Copland.Term]
I
in_cons_app_cons [lemma, in Copland.More_lists]in_skipn_cons [lemma, in Copland.More_lists]
J
join [constructor, in Copland.Term]K
KIM [constructor, in Copland.Term]kk [constructor, in Copland.Term]
kmeas [constructor, in Copland.Term]
L
leaf [constructor, in Copland.Event_system]lin_range [lemma, in Copland.Term]
ls [constructor, in Copland.LTS]
lseq [constructor, in Copland.Term]
lseq_assoc [lemma, in Copland.Term_system]
lstar [inductive, in Copland.LTS]
lstar_rlstar [lemma, in Copland.LTS]
lstar_nlstar_size [lemma, in Copland.LTS]
lstar_nlstar [lemma, in Copland.LTS]
lstar_star [lemma, in Copland.LTS]
lstar_transitive [lemma, in Copland.LTS]
lstar_silent_tran [constructor, in Copland.LTS]
lstar_tran [constructor, in Copland.LTS]
lstar_refl [constructor, in Copland.LTS]
lstar_trace [lemma, in Copland.Main]
LTS [library]
M
Main [library]max [definition, in Copland.Event_system]
max_eval [lemma, in Copland.Term_system]
merge [constructor, in Copland.Event_system]
merge_associative_pairs [lemma, in Copland.Event_system]
merge_associative [lemma, in Copland.Event_system]
More_lists.A [variable, in Copland.More_lists]
More_lists [section, in Copland.More_lists]
More_lists [library]
mt [constructor, in Copland.Term]
N
never_stuck [lemma, in Copland.LTS]nlstar [inductive, in Copland.LTS]
nlstar_step_size [lemma, in Copland.LTS]
nlstar_lstar [lemma, in Copland.LTS]
nlstar_transitive [lemma, in Copland.LTS]
nlstar_silent_tran [constructor, in Copland.LTS]
nlstar_tran [constructor, in Copland.LTS]
nlstar_refl [constructor, in Copland.LTS]
nlstar_trace [lemma, in Copland.Main]
nlstar_trace_helper [lemma, in Copland.Main]
nodup_trace [lemma, in Copland.Trace]
nodup_append [lemma, in Copland.More_lists]
nstar [inductive, in Copland.LTS]
nstar_star [lemma, in Copland.LTS]
nstar_transitive [lemma, in Copland.LTS]
nstar_tran [constructor, in Copland.LTS]
nstar_refl [constructor, in Copland.LTS]
O
ordered [lemma, in Copland.Main]out_ev [definition, in Copland.Term_system]
P
pl [constructor, in Copland.Term]pl [definition, in Copland.LTS]
Plc [abbreviation, in Copland.Term]
pp [constructor, in Copland.Term]
Preamble [library]
prec [inductive, in Copland.Event_system]
prec_in_right [lemma, in Copland.Event_system]
prec_in_left [lemma, in Copland.Event_system]
prparl [constructor, in Copland.Event_system]
prparr [constructor, in Copland.Event_system]
prseq [constructor, in Copland.Event_system]
prseql [constructor, in Copland.Event_system]
prseqr [constructor, in Copland.Event_system]
R
range [definition, in Copland.Term]Range [definition, in Copland.Term]
rem [constructor, in Copland.LTS]
req [constructor, in Copland.Term]
rlstar [inductive, in Copland.LTS]
rlstar_nlstar [lemma, in Copland.LTS]
rlstar_lstar [lemma, in Copland.LTS]
rlstar_transitive [lemma, in Copland.LTS]
rlstar_silent_tran [constructor, in Copland.LTS]
rlstar_tran [constructor, in Copland.LTS]
rlstar_refl [constructor, in Copland.LTS]
rpy [constructor, in Copland.Term]
S
same_rel [definition, in Copland.Event_system]seval [definition, in Copland.LTS]
shuffle [inductive, in Copland.Trace]
shuffle_nodup_append [lemma, in Copland.Trace]
shuffle_earlier_right [lemma, in Copland.Trace]
shuffle_earlier_left [lemma, in Copland.Trace]
shuffle_in_skipn_right [lemma, in Copland.Trace]
shuffle_in_skipn_left [lemma, in Copland.Trace]
shuffle_in [lemma, in Copland.Trace]
shuffle_in_right [lemma, in Copland.Trace]
shuffle_in_left [lemma, in Copland.Trace]
shuffle_length [lemma, in Copland.Trace]
shuffle_right [constructor, in Copland.Trace]
shuffle_left [constructor, in Copland.Trace]
shuffle_nil_right [constructor, in Copland.Trace]
shuffle_nil_left [constructor, in Copland.Trace]
SIG [constructor, in Copland.Term]
sign [constructor, in Copland.Term]
skipn_zero [lemma, in Copland.More_lists]
skipn_in [lemma, in Copland.More_lists]
skipn_all_n [lemma, in Copland.More_lists]
skipn_nil [lemma, in Copland.More_lists]
skipn_all [lemma, in Copland.More_lists]
skipn_append [lemma, in Copland.More_lists]
skipn_app [lemma, in Copland.More_lists]
sp [constructor, in Copland.Term]
split [constructor, in Copland.Term]
Split [definition, in Copland.Term]
ss [constructor, in Copland.Term]
ssize [definition, in Copland.LTS]
St [inductive, in Copland.LTS]
star [inductive, in Copland.LTS]
star_nstar [lemma, in Copland.LTS]
star_stbp [lemma, in Copland.LTS]
star_stbsr [lemma, in Copland.LTS]
star_stbsl [lemma, in Copland.LTS]
star_stls [lemma, in Copland.LTS]
star_strem [lemma, in Copland.LTS]
star_seval [lemma, in Copland.LTS]
star_lstar [lemma, in Copland.LTS]
star_transitive [lemma, in Copland.LTS]
star_tran [constructor, in Copland.LTS]
star_refl [constructor, in Copland.LTS]
stasp [constructor, in Copland.LTS]
statt [constructor, in Copland.LTS]
stattstep [constructor, in Copland.LTS]
stattstop [constructor, in Copland.LTS]
stbpar [constructor, in Copland.LTS]
stbpstepleft [constructor, in Copland.LTS]
stbpstepright [constructor, in Copland.LTS]
stbpstop [constructor, in Copland.LTS]
stbseq [constructor, in Copland.LTS]
stbslstep [constructor, in Copland.LTS]
stbslstop [constructor, in Copland.LTS]
stbsrstep [constructor, in Copland.LTS]
stbsrstop [constructor, in Copland.LTS]
step [inductive, in Copland.LTS]
steps_to_stop [lemma, in Copland.LTS]
steps_preserves_eval [lemma, in Copland.LTS]
step_count [lemma, in Copland.LTS]
step_size [lemma, in Copland.LTS]
step_seval [lemma, in Copland.LTS]
step_pl_eq [lemma, in Copland.LTS]
step_evt_tr [lemma, in Copland.Main]
step_silent_tr [lemma, in Copland.Main]
stlseq [constructor, in Copland.LTS]
stlseqstep [constructor, in Copland.LTS]
stlseqstop [constructor, in Copland.LTS]
stop [constructor, in Copland.LTS]
sup [inductive, in Copland.Event_system]
supreme [definition, in Copland.Event_system]
supreme_unique [lemma, in Copland.Term_system]
supreme_max [lemma, in Copland.Event_system]
sup_supreme [lemma, in Copland.Event_system]
sup_merger [constructor, in Copland.Event_system]
sup_mergel [constructor, in Copland.Event_system]
sup_before [constructor, in Copland.Event_system]
sup_leaf [constructor, in Copland.Event_system]
T
tasp [constructor, in Copland.Trace]tatt [constructor, in Copland.Trace]
tbp [constructor, in Copland.Main]
tbpar [constructor, in Copland.Trace]
tbseq [constructor, in Copland.Trace]
tbsl [constructor, in Copland.Main]
tbsr [constructor, in Copland.Main]
tconf [constructor, in Copland.Main]
Term [inductive, in Copland.Term]
Term [library]
Term_system [library]
tls [constructor, in Copland.Main]
tlseq [constructor, in Copland.Trace]
trace [inductive, in Copland.Trace]
Trace [library]
traceS [inductive, in Copland.Main]
trace_order [lemma, in Copland.Trace]
trace_injective_events [lemma, in Copland.Trace]
trace_range_event [lemma, in Copland.Trace]
trace_range [lemma, in Copland.Trace]
trace_events [lemma, in Copland.Trace]
trace_length [lemma, in Copland.Trace]
trem [constructor, in Copland.Main]
tsize [definition, in Copland.LTS]
tstop [constructor, in Copland.Main]
U
umeas [constructor, in Copland.Term]USM [constructor, in Copland.Term]
uu [constructor, in Copland.Term]
W
well_formed_range [lemma, in Copland.Term]well_formed [inductive, in Copland.Term]
well_structured_evsys [lemma, in Copland.Term_system]
well_structured_range [lemma, in Copland.Event_system]
well_structured [inductive, in Copland.Event_system]
wf_bpar [constructor, in Copland.Term]
wf_bseq [constructor, in Copland.Term]
wf_lseq [constructor, in Copland.Term]
wf_att [constructor, in Copland.Term]
wf_asp [constructor, in Copland.Term]
ws_exists [lemma, in Copland.Event_system]
ws_before2 [lemma, in Copland.Event_system]
ws_before1 [lemma, in Copland.Event_system]
ws_merge2 [lemma, in Copland.Event_system]
ws_merge1 [lemma, in Copland.Event_system]
ws_evsys_range [lemma, in Copland.Event_system]
ws_merge [constructor, in Copland.Event_system]
ws_before [constructor, in Copland.Event_system]
ws_leaf_event [constructor, in Copland.Event_system]
Variable Index
E
Event_system.ev [in Copland.Event_system]Event_system.A [in Copland.Event_system]
M
More_lists.A [in Copland.More_lists]Library Index
E
Event_systemL
LTSM
MainMore_lists
P
PreambleT
TermTerm_system
Trace
Lemma Index
A
anno_well_formed [in Copland.Term]anno_range [in Copland.Term]
at_range [in Copland.Term]
B
before_sup [in Copland.Event_system]before_associative_pairs [in Copland.Event_system]
before_associative [in Copland.Event_system]
bra_range [in Copland.Term]
C
correct_path_exists [in Copland.LTS]E
earlier_cons_shift [in Copland.More_lists]earlier_cons [in Copland.More_lists]
earlier_append_iff [in Copland.More_lists]
earlier_append [in Copland.More_lists]
earlier_right [in Copland.More_lists]
earlier_left [in Copland.More_lists]
earlier_in_right [in Copland.More_lists]
earlier_in_left [in Copland.More_lists]
esizeS_tr [in Copland.Main]
esize_tr [in Copland.Main]
es_injective_events [in Copland.Event_system]
eval_aeval [in Copland.Term]
events_injective [in Copland.Term]
events_range_event [in Copland.Term]
events_range [in Copland.Term]
evsys_max_unique [in Copland.Term_system]
evsys_events [in Copland.Term_system]
evsys_range [in Copland.Term_system]
evsys_transitive [in Copland.Event_system]
evsys_irreflexive [in Copland.Event_system]
evsys_tr_in [in Copland.Trace]
F
firstn_in [in Copland.More_lists]firstn_all_n [in Copland.More_lists]
firstn_append [in Copland.More_lists]
H
halt_size [in Copland.LTS]I
in_cons_app_cons [in Copland.More_lists]in_skipn_cons [in Copland.More_lists]
L
lin_range [in Copland.Term]lseq_assoc [in Copland.Term_system]
lstar_rlstar [in Copland.LTS]
lstar_nlstar_size [in Copland.LTS]
lstar_nlstar [in Copland.LTS]
lstar_star [in Copland.LTS]
lstar_transitive [in Copland.LTS]
lstar_trace [in Copland.Main]
M
max_eval [in Copland.Term_system]merge_associative_pairs [in Copland.Event_system]
merge_associative [in Copland.Event_system]
N
never_stuck [in Copland.LTS]nlstar_step_size [in Copland.LTS]
nlstar_lstar [in Copland.LTS]
nlstar_transitive [in Copland.LTS]
nlstar_trace [in Copland.Main]
nlstar_trace_helper [in Copland.Main]
nodup_trace [in Copland.Trace]
nodup_append [in Copland.More_lists]
nstar_star [in Copland.LTS]
nstar_transitive [in Copland.LTS]
O
ordered [in Copland.Main]P
prec_in_right [in Copland.Event_system]prec_in_left [in Copland.Event_system]
R
rlstar_nlstar [in Copland.LTS]rlstar_lstar [in Copland.LTS]
rlstar_transitive [in Copland.LTS]
S
shuffle_nodup_append [in Copland.Trace]shuffle_earlier_right [in Copland.Trace]
shuffle_earlier_left [in Copland.Trace]
shuffle_in_skipn_right [in Copland.Trace]
shuffle_in_skipn_left [in Copland.Trace]
shuffle_in [in Copland.Trace]
shuffle_in_right [in Copland.Trace]
shuffle_in_left [in Copland.Trace]
shuffle_length [in Copland.Trace]
skipn_zero [in Copland.More_lists]
skipn_in [in Copland.More_lists]
skipn_all_n [in Copland.More_lists]
skipn_nil [in Copland.More_lists]
skipn_all [in Copland.More_lists]
skipn_append [in Copland.More_lists]
skipn_app [in Copland.More_lists]
star_nstar [in Copland.LTS]
star_stbp [in Copland.LTS]
star_stbsr [in Copland.LTS]
star_stbsl [in Copland.LTS]
star_stls [in Copland.LTS]
star_strem [in Copland.LTS]
star_seval [in Copland.LTS]
star_lstar [in Copland.LTS]
star_transitive [in Copland.LTS]
steps_to_stop [in Copland.LTS]
steps_preserves_eval [in Copland.LTS]
step_count [in Copland.LTS]
step_size [in Copland.LTS]
step_seval [in Copland.LTS]
step_pl_eq [in Copland.LTS]
step_evt_tr [in Copland.Main]
step_silent_tr [in Copland.Main]
supreme_unique [in Copland.Term_system]
supreme_max [in Copland.Event_system]
sup_supreme [in Copland.Event_system]
T
trace_order [in Copland.Trace]trace_injective_events [in Copland.Trace]
trace_range_event [in Copland.Trace]
trace_range [in Copland.Trace]
trace_events [in Copland.Trace]
trace_length [in Copland.Trace]
W
well_formed_range [in Copland.Term]well_structured_evsys [in Copland.Term_system]
well_structured_range [in Copland.Event_system]
ws_exists [in Copland.Event_system]
ws_before2 [in Copland.Event_system]
ws_before1 [in Copland.Event_system]
ws_merge2 [in Copland.Event_system]
ws_merge1 [in Copland.Event_system]
ws_evsys_range [in Copland.Event_system]
Constructor Index
A
aasp [in Copland.Term]aatt [in Copland.Term]
abpar [in Copland.Term]
abseq [in Copland.Term]
alseq [in Copland.Term]
arg [in Copland.Term]
asp [in Copland.Term]
att [in Copland.Term]
B
before [in Copland.Event_system]bp [in Copland.LTS]
bpar [in Copland.Term]
bseq [in Copland.Term]
bsl [in Copland.LTS]
bsr [in Copland.LTS]
C
conf [in Copland.LTS]copy [in Copland.Term]
CPY [in Copland.Term]
E
ein_merger [in Copland.Event_system]ein_mergel [in Copland.Event_system]
ein_beforer [in Copland.Event_system]
ein_beforel [in Copland.Event_system]
ein_leaf [in Copland.Event_system]
evtsatt [in Copland.Term]
evtsattreq [in Copland.Term]
evtsattrpy [in Copland.Term]
evtsbparjoin [in Copland.Term]
evtsbparl [in Copland.Term]
evtsbparr [in Copland.Term]
evtsbparsplit [in Copland.Term]
evtsbseqjoin [in Copland.Term]
evtsbseql [in Copland.Term]
evtsbseqr [in Copland.Term]
evtsbseqsplit [in Copland.Term]
evtscpy [in Copland.Term]
evtshsh [in Copland.Term]
evtskim [in Copland.Term]
evtslseql [in Copland.Term]
evtslseqr [in Copland.Term]
evtssig [in Copland.Term]
evtsusm [in Copland.Term]
G
gg [in Copland.Term]H
hash [in Copland.Term]hh [in Copland.Term]
HSH [in Copland.Term]
J
join [in Copland.Term]K
KIM [in Copland.Term]kk [in Copland.Term]
kmeas [in Copland.Term]
L
leaf [in Copland.Event_system]ls [in Copland.LTS]
lseq [in Copland.Term]
lstar_silent_tran [in Copland.LTS]
lstar_tran [in Copland.LTS]
lstar_refl [in Copland.LTS]
M
merge [in Copland.Event_system]mt [in Copland.Term]
N
nlstar_silent_tran [in Copland.LTS]nlstar_tran [in Copland.LTS]
nlstar_refl [in Copland.LTS]
nstar_tran [in Copland.LTS]
nstar_refl [in Copland.LTS]
P
pl [in Copland.Term]pp [in Copland.Term]
prparl [in Copland.Event_system]
prparr [in Copland.Event_system]
prseq [in Copland.Event_system]
prseql [in Copland.Event_system]
prseqr [in Copland.Event_system]
R
rem [in Copland.LTS]req [in Copland.Term]
rlstar_silent_tran [in Copland.LTS]
rlstar_tran [in Copland.LTS]
rlstar_refl [in Copland.LTS]
rpy [in Copland.Term]
S
shuffle_right [in Copland.Trace]shuffle_left [in Copland.Trace]
shuffle_nil_right [in Copland.Trace]
shuffle_nil_left [in Copland.Trace]
SIG [in Copland.Term]
sign [in Copland.Term]
sp [in Copland.Term]
split [in Copland.Term]
ss [in Copland.Term]
star_tran [in Copland.LTS]
star_refl [in Copland.LTS]
stasp [in Copland.LTS]
statt [in Copland.LTS]
stattstep [in Copland.LTS]
stattstop [in Copland.LTS]
stbpar [in Copland.LTS]
stbpstepleft [in Copland.LTS]
stbpstepright [in Copland.LTS]
stbpstop [in Copland.LTS]
stbseq [in Copland.LTS]
stbslstep [in Copland.LTS]
stbslstop [in Copland.LTS]
stbsrstep [in Copland.LTS]
stbsrstop [in Copland.LTS]
stlseq [in Copland.LTS]
stlseqstep [in Copland.LTS]
stlseqstop [in Copland.LTS]
stop [in Copland.LTS]
sup_merger [in Copland.Event_system]
sup_mergel [in Copland.Event_system]
sup_before [in Copland.Event_system]
sup_leaf [in Copland.Event_system]
T
tasp [in Copland.Trace]tatt [in Copland.Trace]
tbp [in Copland.Main]
tbpar [in Copland.Trace]
tbseq [in Copland.Trace]
tbsl [in Copland.Main]
tbsr [in Copland.Main]
tconf [in Copland.Main]
tls [in Copland.Main]
tlseq [in Copland.Trace]
trem [in Copland.Main]
tstop [in Copland.Main]
U
umeas [in Copland.Term]USM [in Copland.Term]
uu [in Copland.Term]
W
wf_bpar [in Copland.Term]wf_bseq [in Copland.Term]
wf_lseq [in Copland.Term]
wf_att [in Copland.Term]
wf_asp [in Copland.Term]
ws_merge [in Copland.Event_system]
ws_before [in Copland.Event_system]
ws_leaf_event [in Copland.Event_system]
Inductive Index
A
AnnoTerm [in Copland.Term]Arg [in Copland.Term]
ASP [in Copland.Term]
E
Ev [in Copland.Term]events [in Copland.Term]
Evidence [in Copland.Term]
EvSys [in Copland.Event_system]
ev_in [in Copland.Event_system]
L
lstar [in Copland.LTS]N
nlstar [in Copland.LTS]nstar [in Copland.LTS]
P
prec [in Copland.Event_system]R
rlstar [in Copland.LTS]S
shuffle [in Copland.Trace]St [in Copland.LTS]
star [in Copland.LTS]
step [in Copland.LTS]
sup [in Copland.Event_system]
T
Term [in Copland.Term]trace [in Copland.Trace]
traceS [in Copland.Main]
W
well_formed [in Copland.Term]well_structured [in Copland.Event_system]
Section Index
E
Event_system [in Copland.Event_system]M
More_lists [in Copland.More_lists]Abbreviation Index
P
Plc [in Copland.Term]Definition Index
A
aeval [in Copland.Term]anno [in Copland.Term]
annotated [in Copland.Term]
asp_event [in Copland.Term]
D
disjoint_lists [in Copland.More_lists]E
earlier [in Copland.More_lists]eq_ev_dec [in Copland.Term]
eq_arg_dec [in Copland.Term]
esize [in Copland.Term]
esizeS [in Copland.Main]
es_size [in Copland.Event_system]
es_range [in Copland.Event_system]
ES_Range [in Copland.Event_system]
ev [in Copland.Term]
eval [in Copland.Term]
eval_asp [in Copland.Term]
ev_sys [in Copland.Term_system]
H
halt [in Copland.LTS]M
max [in Copland.Event_system]O
out_ev [in Copland.Term_system]P
pl [in Copland.LTS]R
range [in Copland.Term]Range [in Copland.Term]
S
same_rel [in Copland.Event_system]seval [in Copland.LTS]
Split [in Copland.Term]
ssize [in Copland.LTS]
supreme [in Copland.Event_system]
T
tsize [in Copland.LTS]| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (308 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (113 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (129 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (23 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (29 entries) |
This page has been generated by coqdoc