Skip to content

GitLab

Commit 25f1b889 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Document why cofe_fun is a definition.

parent 51b15fdc
Show whitespace changes
Inline Side-by-side
algebra/cofe.v
View file @ 25f1b889
...@@ -208,6 +208,8 @@ Section fixpoint. ...@@ -208,6 +208,8 @@ Section fixpoint.
End fixpoint. End fixpoint.
(** Function space *) (** Function space *)
(* We make [cofe_fun] a definition so that we can register it as a canonical
structure. *)
Definition cofe_fun (A : Type) (B : cofeT) := A → B. Definition cofe_fun (A : Type) (B : cofeT) := A → B.
Section cofe_fun. Section cofe_fun.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment