Built with
Alectryon, running Coq+SerAPI v8.15.0+0.15.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl.
(** * Model of Time *)
(** Prosa is based on a discrete model of time. Thus, time is simply defined by
the natural numbers. To aid readability, we distinguish between values of time
that represent a duration and values of time that represent a specific
instant. *)
Definition duration := nat.
Definition instant := nat.