pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Polymorphism: 8.10 update

Browse source
This commit is contained in:
Adam Chlipala 2020-02-04 17:46:37 -05:00
parent 152b90e9ef
commit 295e095e98
2 changed files with 8 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
Polymorphism.v
View file

@ -24,7 +24,7 @@ Inductive option (A : Set) : Set :=
| None
| Some (v : A).
Arguments None [A].
Arguments None {A}.
(* This command asks Coq to *infer* the [A] type for each specific use of
* [None]. *)
@ -61,7 +61,7 @@ Inductive list (A : Set) : Set :=
| nil
| cons (hd : A) (tl : list A).
Arguments nil [A].
Arguments nil {A}.
(* [nil] is the empty list, while [cons], standing for "construct," extends a
* list of length [n] into one of length [n+1]. *)
@ -346,7 +346,7 @@ Inductive tree (A : Set) : Set :=
| Leaf
| Node (l : tree A) (d : A) (r : tree A).
Arguments Leaf [A].
Arguments Leaf {A}.
Example tr1 : tree nat := Node (Node Leaf 7 Leaf) 8 (Node Leaf 9 (Node Leaf 10 Leaf)).
@ -448,6 +448,7 @@ Inductive statement : Set :=
* almost-natural-looking embedded programs in Coq. *)
Coercion Const : nat >-> expression.
Coercion Var : string >-> expression.
Declare Scope embedded_scope.
Infix "+" := Plus : embedded_scope.
Infix "-" := Minus : embedded_scope.
Infix "*" := Times : embedded_scope.

7
Polymorphism_template.v
View file

@ -13,7 +13,7 @@ Inductive option (A : Set) : Set :=
| None
| Some (v : A).
Arguments None [A].
Arguments None {A}.
(* This command asks Coq to *infer* the [A] type for each specific use of
* [None]. *)
@ -50,7 +50,7 @@ Inductive list (A : Set) : Set :=
| nil
| cons (hd : A) (tl : list A).
Arguments nil [A].
Arguments nil {A}.
(* [nil] is the empty list, while [cons], standing for "construct," extends a
* list of length [n] into one of length [n+1]. *)
@ -222,7 +222,7 @@ Inductive tree (A : Set) : Set :=
| Leaf
| Node (l : tree A) (d : A) (r : tree A).
Arguments Leaf [A].
Arguments Leaf {A}.
Example tr1 : tree nat := Node (Node Leaf 7 Leaf) 8 (Node Leaf 9 (Node Leaf 10 Leaf)).
@ -291,6 +291,7 @@ Inductive statement : Set :=
* almost-natural-looking embedded programs in Coq. *)
Coercion Const : nat >-> expression.
Coercion Var : string >-> expression.
Declare Scope embedded_scope.
Infix "+" := Plus : embedded_scope.
Infix "-" := Minus : embedded_scope.
Infix "*" := Times : embedded_scope.