4 ms·
(** A particular execution, defined by a possibly infinite sequence of events from a starting configuration C is called a schedule and the sequence of step
by gergoerdi 11y ago
(** A particular execution, defined by a possibly infinite sequence of events from
a starting configuration C is called a schedule and the sequence of steps taken
to realise the schedule is a run **)
Definition Schedule := list nat.
Is `list` codata by default in Coq?
- CHY872 11y agoDon't you want https://coq.inria.fr/library/Coq.Lists.Streams.html https://coq.inria.fr/library/Coq.Lists.Streams.html ?
- kushti 11y agolist is inductive type for sure, not coinductive. But it could be used for modelling infinite(but countable) sequences in the sense that following property being hold: forall (m:nat), exists (l: list nat), length l > m.