Commit 71dd8f63 authored by Ralf Jung's avatar Ralf Jung
Browse files

make fn_cons universe polymorphic... otherwise, I run into universe errors :-/

parent 37713a6a
...@@ -31,23 +31,19 @@ Section functions. ...@@ -31,23 +31,19 @@ Section functions.
End functions. End functions.
(** "Cons-ing" of functions from nat to T *) (** "Cons-ing" of functions from nat to T *)
Section fcons. Polymorphic Definition fn_cons {T : Type} (t : T) (f: nat T) : nat T :=
Context {T : Type}. λ n, match n with
| O => t
| S n => f n
end.
Definition fn_cons (t : T) (f: nat T) : nat T := Polymorphic Definition fn_mcons {T : Type} (ts : list T) (f : nat T) : nat T :=
λ n, match n with
| O => t
| S n => f n
end.
Definition fn_mcons (ts : list T) (f : nat T) : nat T :=
fold_right fn_cons f ts. fold_right fn_cons f ts.
End fcons.
Infix ".::" := fn_cons (at level 60, right associativity) : C_scope. Infix ".::" := fn_cons (at level 60, right associativity) : C_scope.
Infix ".++" := fn_mcons (at level 60, right associativity) : C_scope. Infix ".++" := fn_mcons (at level 60, right associativity) : C_scope.
Lemma fn_mcons_app {T : Type} (ts1 ts2 : list T) f : Polymorphic Lemma fn_mcons_app {T : Type} (ts1 ts2 : list T) f :
(ts1 ++ ts2) .++ f = ts1 .++ (ts2 .++ f). (ts1 ++ ts2) .++ f = ts1 .++ (ts2 .++ f).
Proof. Proof.
unfold fn_mcons. rewrite fold_right_app. done. unfold fn_mcons. rewrite fold_right_app. done.
......
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