Commit 26691820 authored by Johannes Kloos's avatar Johannes Kloos

Moved Infinite typeclass to infinite

parent 93a88ce7
...@@ -1125,13 +1125,6 @@ Class FreshSpec A C `{ElemOf A C, ...@@ -1125,13 +1125,6 @@ Class FreshSpec A C `{ElemOf A C,
is_fresh (X : C) : fresh X X is_fresh (X : C) : fresh X X
}. }.
(** The class [Infinite] axiomatizes types with infinitely many elements
by giving an injection from the natural numbers into the type. It is mostly
used to provide a generic [fresh] algorithm. *)
Class Infinite A :=
{ inject: nat A;
inject_injective:> Inj (=) (=) inject }.
(** * Miscellaneous *) (** * Miscellaneous *)
Class Half A := half: A A. Class Half A := half: A A.
Hint Mode Half ! : typeclass_instances. Hint Mode Half ! : typeclass_instances.
......
...@@ -2,6 +2,13 @@ ...@@ -2,6 +2,13 @@
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
From stdpp Require Import pretty fin_collections. From stdpp Require Import pretty fin_collections.
(** The class [Infinite] axiomatizes types with infinitely many elements
by giving an injection from the natural numbers into the type. It is mostly
used to provide a generic [fresh] algorithm. *)
Class Infinite A :=
{ inject: nat A;
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 |}.
Instance N_infinite: Infinite N := {| inject_injective := Nat2N.inj |}. Instance N_infinite: Infinite N := {| inject_injective := Nat2N.inj |}.
...@@ -21,4 +28,4 @@ Section StringFresh. ...@@ -21,4 +28,4 @@ Section StringFresh.
Context `{FinCollection string C, (x: string) (s: C), Decision (x s)}. Context `{FinCollection string C, (x: string) (s: C), Decision (x s)}.
Global Instance string_fresh: Fresh string C := fresh_generic. Global Instance string_fresh: Fresh string C := fresh_generic.
Global Instance string_fresh_spec: FreshSpec string C := _. Global Instance string_fresh_spec: FreshSpec string C := _.
End StringFresh. End StringFresh.
\ No newline at end of file
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