1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
Require Import Coq.Strings.Ascii.
Require Import Coq.Strings.String.
Set Implicit Arguments.
Set Maximal Implicit Insertion.
Polymorphic Class Injection (x : Type) (t : Type) := inject : x -> t.
(*
Class Projection x t := { project : t -> x ; pmodify : (x -> x) -> (t -> t) }.
*)
#[global]
Polymorphic Instance Injection_refl {T : Type} : Injection T T :=
{ inject := @id T }.
#[global]
Instance Injection_ascii_string : Injection ascii string :=
{ inject a := String a EmptyString }.
#[global]
Instance Injection_ascii_string_cons : Injection ascii (string -> string) :=
{ inject := String }.
|
