Commit 6ab381a8 authored by Ralf Jung's avatar Ralf Jung
Browse files

coqdoc

parent 6d849e7d
...@@ -26,7 +26,7 @@ Definition from_option {A B} (f : A → B) (y : B) (mx : option A) : B := ...@@ -26,7 +26,7 @@ Definition from_option {A B} (f : A → B) (y : B) (mx : option A) : B :=
Instance: Params (@from_option) 3. Instance: Params (@from_option) 3.
Arguments from_option {_ _} _ _ !_ / : assert. Arguments from_option {_ _} _ _ !_ / : assert.
(* The eliminator with the identity function. *) (** The eliminator with the identity function. *)
Notation default := (from_option id). Notation default := (from_option id).
(** An alternative, but equivalent, definition of equality on the option (** An alternative, but equivalent, definition of equality on the option
......
Markdown is supported
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