Skip to content
Snippets Groups Projects
Commit c36246fc authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

More consistent indentation in `infinite`.

parent 7d49702c
No related branches found
No related tags found
No related merge requests found
...@@ -6,9 +6,10 @@ From stdpp Require Import pretty relations. ...@@ -6,9 +6,10 @@ From stdpp Require Import pretty relations.
(** The class [Infinite] axiomatizes types with infinitely many elements (** The class [Infinite] axiomatizes types with infinitely many elements
by giving an injection from the natural numbers into the type. It is mostly by giving an injection from the natural numbers into the type. It is mostly
used to provide a generic [fresh] algorithm. *) used to provide a generic [fresh] algorithm. *)
Class Infinite A := Class Infinite A := {
{ inject: nat A; inject: nat A;
inject_injective:> Inj (=) (=) inject }. inject_injective :> Inj (=) (=) inject;
}.
Instance string_infinite: Infinite string := {| inject := λ x, "~" +:+ pretty x |}. Instance string_infinite: Infinite string := {| inject := λ x, "~" +:+ pretty x |}.
Instance nat_infinite: Infinite nat := {| inject := id |}. Instance nat_infinite: Infinite nat := {| inject := id |}.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment