Unverified Commit b7f57848 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Bad fix (to replace with Janno's)

parent 09b6a0c3
Pipeline #66059 passed with stage
in 7 minutes and 59 seconds
......@@ -6,10 +6,10 @@ Import bi.
(* This cannot import the proofmode because it is imported by the proofmode! *)
(** Telescopic quantifiers *)
Definition bi_texist {PROP : bi} {TT : tele@{Quant}} (Ψ : TT PROP) : PROP :=
Definition bi_texist {PROP : bi} {TT : tele} (Ψ : TT PROP) : PROP :=
tele_fold (@bi_exist PROP) (λ x, x) (tele_bind Ψ).
Global Arguments bi_texist {_ !_} _ /.
Definition bi_tforall {PROP : bi} {TT : tele@{Quant}} (Ψ : TT PROP) : PROP :=
Definition bi_tforall {PROP : bi} {TT : tele} (Ψ : TT PROP) : PROP :=
tele_fold (@bi_forall PROP) (λ x, x) (tele_bind Ψ).
Global Arguments bi_tforall {_ !_} _ /.
......@@ -21,7 +21,7 @@ Notation "'∀..' x .. y , P" := (bi_tforall (λ x, .. (bi_tforall (λ y, P)) ..
format "∀.. x .. y , P") : bi_scope.
Section telescopes.
Context {PROP : bi} {TT : tele@{Quant}}.
Context {PROP : bi} {TT : tele}.
Implicit Types Ψ : TT PROP.
Lemma bi_tforall_forall Ψ : bi_tforall Ψ bi_forall Ψ.
......
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