From d945203bee213ff8ce0e97fd2891030caf3c89ae Mon Sep 17 00:00:00 2001 From: project_18556810_bot Date: Wed, 4 Dec 2024 11:15:30 +0000 Subject: [PATCH] [github pages] BRiCk documentation created from 0ec27097 --- .../bedrock.lang.bi.telescopes.html | 36 +++++++++---------- .../bedrock.lang.cpp.syntax.mtraverse.html | 8 ++--- ....lang.cpp.syntax.name_notation.parser.html | 2 +- .../bedrock.lang.cpp.syntax.preliminary.html | 2 +- .../bedrock.prelude.telescopes.html | 4 +-- .../bedrock.upoly.base.html | 6 ++-- .../bedrock.upoly.prod.html | 2 +- .../bedrock.upoly.html/bedrock.upoly.sum.html | 2 +- 8 files changed, 31 insertions(+), 31 deletions(-) diff --git a/docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.bi.telescopes.html b/docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.bi.telescopes.html index e9ff6f26..e9e359f7 100644 --- a/docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.bi.telescopes.html +++ b/docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.bi.telescopes.html @@ -63,8 +63,8 @@

bedrock.lang.bi.telescopes

polymorphism and a slightly different interface.
-Fixpoint tbi_exist@{X Z Y} {PROP : bi} {t : tele@{X}}
-  : forall (P : tele_fun@{X Z Y} t PROP), PROP :=
+Fixpoint tbi_exist@{X Z Y} {PROP : bi} {t : tele@{X}}
+  : forall (P : tele_fun@{X Z Y} t PROP), PROP :=
  match t as t0 return ((t0 -t> PROP) → PROP) with
  | [tele] => fun x : PROP => x
  | @TeleS X binder =>
@@ -72,8 +72,8 @@

bedrock.lang.bi.telescopes

  end.

-Fixpoint tbi_forall@{X Z Y} {PROP : bi} {t : tele@{X}}
-  : forall (P : tele_fun@{X Z Y} t PROP), PROP :=
+Fixpoint tbi_forall@{X Z Y} {PROP : bi} {t : tele@{X}}
+  : forall (P : tele_fun@{X Z Y} t PROP), PROP :=
  match t as t0 return ((t0 -t> PROP) → PROP) with
  | [tele] => fun x : PROP => x
  | @TeleS X binder =>
@@ -144,7 +144,7 @@

bedrock.lang.bi.telescopes

Avoid the preceding lemmas which would unduly constrain universe Y.
-  Lemma tbi_exist_exist@{X Z Y} {t : tele@{X}} (P : tele_fun@{X Z Y} t PROP) :
+  Lemma tbi_exist_exist@{X Z Y} {t : tele@{X}} (P : tele_fun@{X Z Y} t PROP) :
    tbi_exist P -|- Exists x, tele_app P x.
  Proof.
    induction t as [|B bnd IH]; simpl; split'.
@@ -157,19 +157,19 @@

bedrock.lang.bi.telescopes

  Qed.

-  Lemma tbi_exist_mono@{X Z Y} {t : tele@{X}} (P1 P2 : tele_fun@{X Z Y} t PROP) :
-    tele_fun_pointwise@{X Z Y} (⊢) P1 P2 -> tbi_exist P1 ⊢ tbi_exist P2.
+  Lemma tbi_exist_mono@{X Z Y} {t : tele@{X}} (P1 P2 : tele_fun@{X Z Y} t PROP) :
+    tele_fun_pointwise@{X Z Y} (⊢) P1 P2 -> tbi_exist P1 ⊢ tbi_exist P2.
  Proof. intros. rewrite !tbi_exist_exist. solve_proper. Qed.

-  Lemma tbi_exist_ne@{X Z Y} {t : tele@{X}} n (P1 P2 : tele_fun@{X Z Y} t PROP) :
-    tele_fun_pointwise@{X Z Y} (dist n) P1 P2 ->
+  Lemma tbi_exist_ne@{X Z Y} {t : tele@{X}} n (P1 P2 : tele_fun@{X Z Y} t PROP) :
+    tele_fun_pointwise@{X Z Y} (dist n) P1 P2 ->
    dist n (tbi_exist P1) (tbi_exist P2).
  Proof. intros. rewrite !tbi_exist_exist. solve_proper. Qed.

-  Lemma tbi_exist_proper@{X Z Y} {t : tele@{X}} (P1 P2 : tele_fun@{X Z Y} t PROP) :
-    tele_fun_pointwise@{X Z Y} equiv P1 P2 ->
+  Lemma tbi_exist_proper@{X Z Y} {t : tele@{X}} (P1 P2 : tele_fun@{X Z Y} t PROP) :
+    tele_fun_pointwise@{X Z Y} equiv P1 P2 ->
    equiv (tbi_exist P1) (tbi_exist P2).
  Proof. intros. rewrite !tbi_exist_exist. solve_proper. Qed.
@@ -180,7 +180,7 @@

bedrock.lang.bi.telescopes

  Proof. rewrite tbi_forall_bi_tforall. f_equiv=>x. by rewrite tele_app_bind. Qed.

-  Lemma tbi_forall_forall@{X Z Y} {t : tele@{X}} (P : tele_fun@{X Z Y} t PROP) :
+  Lemma tbi_forall_forall@{X Z Y} {t : tele@{X}} (P : tele_fun@{X Z Y} t PROP) :
    tbi_forall P -|- Forall x, tele_app P x.
  Proof.
    induction t as [|B bnd IH]; simpl; split'.
@@ -193,19 +193,19 @@

bedrock.lang.bi.telescopes

  Qed.

-  Lemma tbi_forall_mono@{X Z Y} {t : tele@{X}} (P1 P2 : tele_fun@{X Z Y} t PROP) :
-    tele_fun_pointwise@{X Z Y} (⊢) P1 P2 -> tbi_forall P1 ⊢ tbi_forall P2.
+  Lemma tbi_forall_mono@{X Z Y} {t : tele@{X}} (P1 P2 : tele_fun@{X Z Y} t PROP) :
+    tele_fun_pointwise@{X Z Y} (⊢) P1 P2 -> tbi_forall P1 ⊢ tbi_forall P2.
  Proof. intros. rewrite !tbi_forall_forall. solve_proper. Qed.

-  Lemma tbi_forall_ne@{X Z Y} {t : tele@{X}} n (P1 P2 : tele_fun@{X Z Y} t PROP) :
-    tele_fun_pointwise@{X Z Y} (dist n) P1 P2 ->
+  Lemma tbi_forall_ne@{X Z Y} {t : tele@{X}} n (P1 P2 : tele_fun@{X Z Y} t PROP) :
+    tele_fun_pointwise@{X Z Y} (dist n) P1 P2 ->
    dist n (tbi_forall P1) (tbi_forall P2).
  Proof. intros. rewrite !tbi_forall_forall. solve_proper. Qed.

-  Lemma tbi_forall_proper@{X Z Y} {t : tele@{X}} (P1 P2 : tele_fun@{X Z Y} t PROP) :
-    tele_fun_pointwise@{X Z Y} equiv P1 P2 ->
+  Lemma tbi_forall_proper@{X Z Y} {t : tele@{X}} (P1 P2 : tele_fun@{X Z Y} t PROP) :
+    tele_fun_pointwise@{X Z Y} equiv P1 P2 ->
    equiv (tbi_forall P1) (tbi_forall P2).
  Proof. intros. rewrite !tbi_forall_forall. solve_proper. Qed.
diff --git a/docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.cpp.syntax.mtraverse.html b/docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.cpp.syntax.mtraverse.html index 9b6a16a7..7f05e20a 100644 --- a/docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.cpp.syntax.mtraverse.html +++ b/docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.cpp.syntax.mtraverse.html @@ -94,9 +94,9 @@

bedrock.lang.cpp.syntax.mtraverse


  Context {F : Type@{u1} -> Type@{u2}}.
-  Context `{!FMap@{u1 u2 uB} F}.
+  Context `{!FMap@{u1 u2 uB} F}.
  Context `{!MRet F, !MFail F}.
-  Context `{AP : !Ap@{u1 u2 uA uB} F}.
+  Context `{AP : !Ap@{u1 u2 uA uB} F}.

  Definition option_traverse2@{uC | uC <= uA , uC <= uB}
@@ -127,9 +127,9 @@

bedrock.lang.cpp.syntax.mtraverse


  Context {F : Type@{u1} -> Type@{u2}}.
-  Context `{!FMap@{u1 u2 uB} F}.
+  Context `{!FMap@{u1 u2 uB} F}.
  Context `{!MRet F, !MFail F}.
-  Context `{AP : !Ap@{u1 u2 uA uB} F}.
+  Context `{AP : !Ap@{u1 u2 uA uB} F}.

  Definition list_traverse2@{uC | uC <= uA , uC <= uB}
diff --git a/docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.cpp.syntax.name_notation.parser.html b/docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.cpp.syntax.name_notation.parser.html index 0e30ae0f..aa496867 100644 --- a/docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.cpp.syntax.name_notation.parser.html +++ b/docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.cpp.syntax.name_notation.parser.html @@ -91,7 +91,7 @@

bedrock.lang.cpp.syntax.name_notation.parser

    Context {RET : MRet Mbase} {FMAP : FMap Mbase} {AP : Ap Mbase} {MBIND : MBind Mbase}.

-    Notation M := (parsec.M@{Set _ _ _ _ _ _} Byte.byte Mbase).
+    Notation M := (parsec.M@{Set _ _ _ _ _ _} Byte.byte Mbase).

    Definition digit_char (b : Byte.byte) : bool :=
diff --git a/docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.cpp.syntax.preliminary.html b/docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.cpp.syntax.preliminary.html index f32eb1ad..762104c2 100644 --- a/docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.cpp.syntax.preliminary.html +++ b/docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.cpp.syntax.preliminary.html @@ -952,7 +952,7 @@

bedrock.lang.cpp.syntax.preliminary


  (* don't use the notation? *)
  #[universes(polymorphic)]
-  Definition traverse@{u | } {F : Set -> Type@{u}} `{FM: FMap F, AP : !Ap@{Set u Set Set} F}
+  Definition traverse@{u | } {F : Set -> Type@{u}} `{FM: FMap F, AP : !Ap@{Set u Set Set} F}
  {name name' functype functype' Expr Expr' : Set}
  (f : name -> F name') (g : functype -> F functype')
  (h : Expr -> F Expr')
diff --git a/docs/_static/coqdoc/bedrock.prelude.html/bedrock.prelude.telescopes.html b/docs/_static/coqdoc/bedrock.prelude.html/bedrock.prelude.telescopes.html index e608978b..2e390290 100644 --- a/docs/_static/coqdoc/bedrock.prelude.html/bedrock.prelude.telescopes.html +++ b/docs/_static/coqdoc/bedrock.prelude.html/bedrock.prelude.telescopes.html @@ -60,8 +60,8 @@

bedrock.prelude.telescopes

  end.

-Definition tele_fun_pointwise@{X Z Y} {t : tele@{X}} {A : Type@{Z}}
-    (R : A -> A -> Prop) (f g : tele_fun@{X Z Y} t A) : Prop :=
+Definition tele_fun_pointwise@{X Z Y} {t : tele@{X}} {A : Type@{Z}}
+    (R : A -> A -> Prop) (f g : tele_fun@{X Z Y} t A) : Prop :=
  forall x, R (tele_app f x) (tele_app g x).

diff --git a/docs/_static/coqdoc/bedrock.upoly.html/bedrock.upoly.base.html b/docs/_static/coqdoc/bedrock.upoly.html/bedrock.upoly.base.html index 1132fd20..0961c389 100644 --- a/docs/_static/coqdoc/bedrock.upoly.html/bedrock.upoly.base.html +++ b/docs/_static/coqdoc/bedrock.upoly.html/bedrock.upoly.base.html @@ -205,7 +205,7 @@

bedrock.upoly.base


  Class Traverse@{u1 u2 v1 v2 uA uB uB'} (T : Type@{u1} -> Type@{u2}) : Type :=
    traverse : ∀ {F : Type@{v1} -> Type@{v2}}
-      `{!FMap@{v1 v2 uB} F, !MRet@{v1 v2} F, AP : !Ap@{v1 v2 uA uB'} F}
+      `{!FMap@{v1 v2 uB} F, !MRet@{v1 v2} F, AP : !Ap@{v1 v2 uA uB'} F}
       {A : Type@{u1}} {B : Type@{v1}}, (A -> F B) -> T A -> F (T B).
  #[global] Hint Mode Traverse ! : typeclass_instances.
  #[global] Instance traverse_params : Params (@traverse) 8 := {}.
@@ -579,7 +579,7 @@

bedrock.upoly.base

    Constraint uS <= u1.
    Constraint uA <= sum.u0, uA' <= sum.u0, uA' <= uS.
    Constraint uB <= sum.u1, uB' <= sum.u1, uB' <= uS.
-    Context {F : Type@{u1} -> Type@{u2}} `{!FMap@{u1 u2 uS} F, !MRet F}.
+    Context {F : Type@{u1} -> Type@{u2}} `{!FMap@{u1 u2 uS} F, !MRet F}.
    Context {A : Type@{uA}} {B : Type@{uB}} {A' : Type@{uA'}} {B' : Type@{uB'}}.

@@ -643,7 +643,7 @@

bedrock.upoly.base

  Section prod_traverse.
    Universes u1 u2 uL uR.
    Constraint uL <= u1, uR <= u1.
-    Context {F : Type@{u1} -> Type@{u2}} `{!FMap@{u1 u2 uR} F, !MRet F, AP : !Ap@{u1 u2 uL uR} F}.
+    Context {F : Type@{u1} -> Type@{u2}} `{!FMap@{u1 u2 uR} F, !MRet F, AP : !Ap@{u1 u2 uL uR} F}.

    Universes uA uB uA' uB'.
diff --git a/docs/_static/coqdoc/bedrock.upoly.html/bedrock.upoly.prod.html b/docs/_static/coqdoc/bedrock.upoly.html/bedrock.upoly.prod.html index d8528bee..c1e0a538 100644 --- a/docs/_static/coqdoc/bedrock.upoly.html/bedrock.upoly.prod.html +++ b/docs/_static/coqdoc/bedrock.upoly.html/bedrock.upoly.prod.html @@ -112,7 +112,7 @@

bedrock.upoly.prod

Section traverse.
  Universes u1 u2 uL uR.
  Constraint uL <= u1, uR <= u1.
-  Context {F : Type@{u1} -> Type@{u2}} `{!FMap@{u1 u2 uR} F, !MRet F, AP : !Ap@{u1 u2 uL uR} F}.
+  Context {F : Type@{u1} -> Type@{u2}} `{!FMap@{u1 u2 uR} F, !MRet F, AP : !Ap@{u1 u2 uL uR} F}.

  Universes uA uB uA' uB'.
diff --git a/docs/_static/coqdoc/bedrock.upoly.html/bedrock.upoly.sum.html b/docs/_static/coqdoc/bedrock.upoly.html/bedrock.upoly.sum.html index 38e8389b..b5183578 100644 --- a/docs/_static/coqdoc/bedrock.upoly.html/bedrock.upoly.sum.html +++ b/docs/_static/coqdoc/bedrock.upoly.html/bedrock.upoly.sum.html @@ -108,7 +108,7 @@

bedrock.upoly.sum

  Constraint uS <= u1.
  Constraint uA' <= uS.
  Constraint uB' <= uS.
-  Context {F : Type@{u1} -> Type@{u2}} `{!FMap@{u1 u2 uS} F}.
+  Context {F : Type@{u1} -> Type@{u2}} `{!FMap@{u1 u2 uS} F}.
  Context {A : Type@{uA}} {B : Type@{uB}} {A' : Type@{uA'}} {B' : Type@{uB'}}.