Commit 9c37da7e authored by Gregory Malecha's avatar Gregory Malecha Committed by Gregory Malecha
Browse files

Unicode preferences + comments.

parent c558023a
Pipeline #64360 passed with stage
in 5 minutes and 1 second
......@@ -48,6 +48,7 @@ is essentially just a (dependent) product.
*)
Definition no_bump@{u} (t : tele@{u}) : Type@{u} := tele_arg@{u} t.
Lemma texist_exist_universes (X : Type) (P : TeleS (fun _ : X => TeleO) -> Prop) :
texist P <-> ex P.
(** This test would fail without [Unset Universe Minimization ToSet] in [telescopes.v]. *)
Lemma texist_exist_universes (X : Type) (P : TeleS (λ _ : X, TeleO) Prop) :
texist P ex P.
Proof. by rewrite texist_exist. Qed.
......@@ -3,8 +3,9 @@ From stdpp Require Import options.
Local Set Universe Polymorphism.
(* Without this flag, Coq minimizes some universes to [Set] when they
should not be, e.g. in [texist_exist]. *)
(** Without this flag, Coq minimizes some universes to [Set] when they
should not be, e.g. in [texist_exist].
See the [texist_exist_universes] test. *)
Local Unset Universe Minimization ToSet.
(** Telescopes *)
......@@ -75,7 +76,7 @@ Lemma tele_arg_inv {TT : tele} (a : tele_arg TT) :
| TeleS f => λ a, x a', a = TargS x a'
end a.
Proof. destruct TT; destruct a; eauto. Qed.
Lemma tele_arg_O_inv (a : TeleO) : a = ().
Lemma tele_arg_O_inv (a : TeleO) : a = TargO.
Proof. exact (tele_arg_inv a). Qed.
Lemma tele_arg_S_inv {X} {f : X tele} (a : TeleS f) :
x a', a = TargS x a'.
......
Supports Markdown
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