Commit 6e699f67 authored by Gregory Malecha's avatar Gregory Malecha
Browse files

Adding a test file.

parent c74e4be0
Pipeline #62979 canceled with stage
in 1 minute and 42 seconds
......@@ -41,3 +41,9 @@ Notation "'[TEST' x .. z , P ']'" :=
(tele_app (λ x, .. (λ z, P) ..)))
(x binder, z binder).
Check [TEST (x y : nat), x = y].
(* [tele_arg t] should live at the same universe
as the types inside of [t] because [tele_arg t]
is essentially just a (dependent) product. *)
Definition no_bump@{u} (t : tele@{u}) :=
TeleS (fun _ : tele_arg@{u} t => TeleO@{u}).
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