Commit 1aceb4c6 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'janno/fix-TargS-notation' into 'master'

Annotate telescope notations to support literal telescope arguments.

See merge request !375
parents 4fb85912 d1bec90c
Pipeline #65437 passed with stage
in 9 minutes and 12 seconds
......@@ -52,3 +52,30 @@ Definition no_bump@{u} (t : tele@{u}) : Type@{u} := tele_arg@{u} t.
Lemma texist_exist_universes (X : Type) (P : TeleS (λ _ : X, TeleO) Prop) :
texist P ex P.
Proof. by rewrite texist_exist. Qed.
(** [tele_arg ..] notation tests.
These tests mainly test type annotations and casts in the [tele_arg]
We test that Coq can typecheck literal telescope arguments in two ways:
- tactic unification/old unification using [exact]
- evarconv/new unification using [refine]
Example tele_arg_notation_0 : [tele].
assert_succeeds exact [tele_arg].
assert_succeeds refine [tele_arg].
Example tele_arg_notation_1 : [tele (_:nat)].
assert_succeeds exact [tele_arg 0].
assert_succeeds refine [tele_arg 0].
Example tele_arg_notation_2 : [tele (_ : bool) (_ : nat)].
assert_succeeds exact [tele_arg true; 0].
assert_succeeds refine [tele_arg true; 0].
Example tele_arg_notation_2_dep : [tele (b : bool) (_ : if b then nat else False)].
assert_succeeds exact [tele_arg true; 0].
assert_succeeds refine [tele_arg true; 0].
......@@ -52,8 +52,20 @@ Fixpoint tele_arg@{u} (t : tele@{u}) : Type@{u} :=
| TeleS f => tele_arg_cons (λ x, tele_arg (f x))
Global Arguments tele_arg _ : simpl never.
Notation TargO := tt (only parsing).
Notation TargS a b := (@TeleArgCons _ (λ x, tele_arg _) a b) (only parsing).
(* Coq has no idea that [unit] and [tele_arg_cons] have anything to do with
telescopes. This only becomes a problem when concrete telescope arguments
(of concrete telescopes) need to be typechecked. To work around this, we
annotate the notations below with extra information to guide unification.
(* The cast in the notation below is necessary to make Coq understand that
[TargO] can be unified with [tele_arg TeleO]. *)
Notation TargO := (tt : tele_arg TeleO) (only parsing).
(* The casts and annotations are necessary for Coq to typecheck nested [TargS]
as well as the final [TargO] in a chain of [TargS]. *)
Notation TargS a b :=
((@TeleArgCons _ (λ x, tele_arg (_ x)) a b) : (tele_arg (TeleS _))) (only parsing).
Coercion tele_arg : tele >-> Sortclass.
Lemma tele_arg_ind (P : TT, tele_arg TT Prop) :
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