Built with
Alectryon, running Coq+coqc-time vThe Rocq Prover, version 9.1.1
compiled with OCaml 5.2.1. 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.
(* ------------------------------------------------------------------------ *)
(* Adapted from Celsius project : https://github.com/clementblaudeau/celsius *)
(* Typing *)
Reserved Notation "q1 ⊑ q2" (at level 40).
Reserved Notation "T1 <: T2" (at level 40).
(* Updates *)
Reserved Notation "[ x ↦ y ] σ" (at level 0).
Reserved Notation "[ x ⟼ y ] σ" (at level 0).
Notation "'dom' x" := (length x) (at level 0, x at level 1).