Built with
Alectryon, running Coq+SerAPI v8.16.0+0.16.3. 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.
From Tealeaves Require Export
Classes.Functor.
(** * The Identity Functor *)
(**********************************************************************)
#[export] Instance Map_I: Map (fun A => A) :=
fun (A B: Type) (f: A -> B) => f.
#[program, export] Instance Functor_I: Functor (fun A => A).