Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
stdpp
Commits
b0065fea
Commit
b0065fea
authored
May 16, 2022
by
Jan-Oliver Kaiser
Browse files
Move universe-related telescope tests closer together.
parent
8eb17fc8
Pipeline
#66075
passed with stage
in 5 minutes and 11 seconds
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
tests/telescopes.v
View file @
b0065fea
...
...
@@ -2,11 +2,28 @@ From stdpp Require Import tactics telescopes.
Local
Unset
Mangle
Names
.
(* for stable goal printing *)
Section
universes
.
(** 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
.
(** [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
})
:
Type
@{
u
}
:
=
tele_arg
@{
u
}
t
.
(* Assert that telescopes are cumulatively universe polymorphic.
See https://gitlab.mpi-sws.org/iris/iris/-/issues/461
*)
Section
cumulativity
.
Monomorphic
Universes
Quant
local
.
Monomorphic
Constraint
local
<
Quant
.
Example
cumul
(
t
:
tele
@{
local
})
:
tele
@{
Quant
}
:
=
t
.
End
cumulativity
.
End
universes
.
Section
accessor
.
(* This is like Iris' accessors, but in Prop. Just to play with telescopes. *)
Definition
accessor
{
X
:
tele
}
(
α
β
γ
:
X
→
Prop
)
:
Prop
:
=
...
...
@@ -47,12 +64,6 @@ Notation "'[TEST' 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
})
:
Type
@{
u
}
:
=
tele_arg
@{
u
}
t
.
(** [tele_arg ..] notation tests.
These tests mainly test type annotations and casts in the [tele_arg]
notations.
...
...
@@ -79,12 +90,3 @@ 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
].
Abort
.
(* Assert that telescopes are cumulatively universe polymorphic.
See https://gitlab.mpi-sws.org/iris/iris/-/issues/461
*)
Section
Cumulativity
.
Monomorphic
Universes
Quant
local
.
Monomorphic
Constraint
local
<
Quant
.
Example
cumul
(
t
:
tele
@{
local
})
:
tele
@{
Quant
}
:
=
t
.
End
Cumulativity
.
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment