diff --git a/ext/prop-eq/Mcltt.Core.Syntactic.Corollaries.html b/ext/prop-eq/Mcltt.Core.Syntactic.Corollaries.html
index 1fbcc85..c68530c 100644
--- a/ext/prop-eq/Mcltt.Core.Syntactic.Corollaries.html
+++ b/ext/prop-eq/Mcltt.Core.Syntactic.Corollaries.html
@@ -115,7 +115,7 @@
Mcltt.Core.Syntactic.Corollaries
Lemma app_ctx_lookup : forall Δ T Γ n,
length Δ = n ->
- {{ #n : ~(iter (S n) (fun T => {{{T [ Wk ]}}}) T) ∈ ~(Δ ++ T :: Γ) }}.
+ {{ #n : ^(iter (S n) (fun T => {{{T [ Wk ]}}}) T) ∈ ^(Δ ++ T :: Γ) }}.
Proof.
induction Δ; intros; simpl in *; subst; mauto.
Qed.
@@ -133,9 +133,9 @@ Mcltt.Core.Syntactic.Corollaries
Lemma app_ctx_vlookup : forall Δ T Γ n,
- {{ ⊢ ~(Δ ++ T :: Γ) }} ->
+ {{ ⊢ ^(Δ ++ T :: Γ) }} ->
length Δ = n ->
- {{ ~(Δ ++ T :: Γ) ⊢ #n : ~(iter (S n) (fun T => {{{T [ Wk ]}}}) T) }}.
+ {{ ^(Δ ++ T :: Γ) ⊢ #n : ^(iter (S n) (fun T => {{{T [ Wk ]}}}) T) }}.
Proof.
intros. econstructor; auto using app_ctx_lookup.
Qed.
diff --git a/ext/prop-eq/Mcltt.Core.Syntactic.CtxSub.html b/ext/prop-eq/Mcltt.Core.Syntactic.CtxSub.html
index 96ab9b8..13afcad 100644
--- a/ext/prop-eq/Mcltt.Core.Syntactic.CtxSub.html
+++ b/ext/prop-eq/Mcltt.Core.Syntactic.CtxSub.html
@@ -50,11 +50,11 @@ Mcltt.Core.Syntactic.CtxSub
#[local]
Ltac gen_ctxsub_helper_IH ctxsub_exp_helper ctxsub_exp_eq_helper ctxsub_sub_helper ctxsub_sub_eq_helper ctxsub_subtyp_helper H :=
match type of H with
- | {{ ~?Γ ⊢ ~?M : ~?A }} => pose proof ctxsub_exp_helper _ _ _ H
- | {{ ~?Γ ⊢ ~?M ≈ ~?N : ~?A }} => pose proof ctxsub_exp_eq_helper _ _ _ _ H
- | {{ ~?Γ ⊢s ~?σ : ~?Δ }} => pose proof ctxsub_sub_helper _ _ _ H
- | {{ ~?Γ ⊢s ~?σ ≈ ~?τ : ~?Δ }} => pose proof ctxsub_sub_eq_helper _ _ _ _ H
- | {{ ~?Γ ⊢ ~?M ⊆ ~?M' }} => pose proof ctxsub_subtyp_helper _ _ _ H
+ | {{ ^?Γ ⊢ ^?M : ^?A }} => pose proof ctxsub_exp_helper _ _ _ H
+ | {{ ^?Γ ⊢ ^?M ≈ ^?N : ^?A }} => pose proof ctxsub_exp_eq_helper _ _ _ _ H
+ | {{ ^?Γ ⊢s ^?σ : ^?Δ }} => pose proof ctxsub_sub_helper _ _ _ H
+ | {{ ^?Γ ⊢s ^?σ ≈ ^?τ : ^?Δ }} => pose proof ctxsub_sub_eq_helper _ _ _ _ H
+ | {{ ^?Γ ⊢ ^?M ⊆ ^?M' }} => pose proof ctxsub_subtyp_helper _ _ _ H
end.
diff --git a/ext/prop-eq/Mcltt.Core.Syntactic.Presup.html b/ext/prop-eq/Mcltt.Core.Syntactic.Presup.html
index aca2de7..af6d673 100644
--- a/ext/prop-eq/Mcltt.Core.Syntactic.Presup.html
+++ b/ext/prop-eq/Mcltt.Core.Syntactic.Presup.html
@@ -37,11 +37,11 @@ Mcltt.Core.Syntactic.Presup
#[local]
Ltac gen_presup_ctx H :=
match type of H with
- | {{ ⊢ ~?Γ ≈ ~?Δ }} =>
+ | {{ ⊢ ^?Γ ≈ ^?Δ }} =>
let HΓ := fresh "HΓ" in
let HΔ := fresh "HΔ" in
pose proof presup_ctx_eq H as [HΓ HΔ]
- | {{ ⊢ ~?Γ ⊆ ~?Δ }} =>
+ | {{ ⊢ ^?Γ ⊆ ^?Δ }} =>
let HΓ := fresh "HΓ" in
let HΔ := fresh "HΔ" in
pose proof presup_ctx_sub H as [HΓ HΔ]
@@ -51,31 +51,31 @@ Mcltt.Core.Syntactic.Presup
#[local]
Ltac gen_presup_IH presup_exp_eq presup_sub_eq presup_subtyp H :=
match type of H with
- | {{ ~?Γ ⊢ ~?M ≈ ~?N : ~?A }} =>
+ | {{ ^?Γ ⊢ ^?M ≈ ^?N : ^?A }} =>
let HΓ := fresh "HΓ" in
let i := fresh "i" in
let HM := fresh "HM" in
let HN := fresh "HN" in
let HAi := fresh "HAi" in
pose proof presup_exp_eq _ _ _ _ H as [HΓ [HM [HN [i HAi]]]]
- | {{ ~?Γ ⊢s ~?σ ≈ ~?τ : ~?Δ }} =>
+ | {{ ^?Γ ⊢s ^?σ ≈ ^?τ : ^?Δ }} =>
let HΓ := fresh "HΓ" in
let Hσ := fresh "Hσ" in
let Hτ := fresh "Hτ" in
let HΔ := fresh "HΔ" in
pose proof presup_sub_eq _ _ _ _ H as [HΓ [Hσ [Hτ HΔ]]]
- | {{ ~?Γ ⊢ ~?M ⊆ ~?N }} =>
+ | {{ ^?Γ ⊢ ^?M ⊆ ^?N }} =>
let HΓ := fresh "HΓ" in
let i := fresh "i" in
let HM := fresh "HM" in
let HN := fresh "HN" in
pose proof presup_subtyp _ _ _ H as [HΓ [i [HM HN]]]
- | {{ ~?Γ ⊢ ~?M : ~?A }} =>
+ | {{ ^?Γ ⊢ ^?M : ^?A }} =>
let HΓ := fresh "HΓ" in
let i := fresh "i" in
let HAi := fresh "HAi" in
pose proof presup_exp H as [HΓ [i HAi]]
- | {{ ~?Γ ⊢s ~?σ : ~?Δ }} =>
+ | {{ ^?Γ ⊢s ^?σ : ^?Δ }} =>
let HΓ := fresh "HΓ" in
let HΔ := fresh "HΔ" in
pose proof presup_sub H as [HΓ HΔ]
diff --git a/ext/prop-eq/Mcltt.Core.Syntactic.Syntax.html b/ext/prop-eq/Mcltt.Core.Syntactic.Syntax.html
index 295e549..2c9cfdd 100644
--- a/ext/prop-eq/Mcltt.Core.Syntactic.Syntax.html
+++ b/ext/prop-eq/Mcltt.Core.Syntactic.Syntax.html
@@ -263,7 +263,7 @@ Mcltt.Core.Syntactic.Syntax
Notation "e [ s ]" := (
a_sub e s) (
in custom exp at level 0,
e custom exp,
s custom exp at level 60,
left associativity,
format "e [ s ]") :
mcltt_scope.
Notation "( x )" :=
x (
in custom exp at level 0,
x custom exp at level 60) :
mcltt_scope.
-
Notation "~ x" :=
x (
in custom exp at level 0,
x constr at level 0) :
mcltt_scope.
+
Notation "'^' x" :=
x (
in custom exp at level 0,
x constr at level 0) :
mcltt_scope.
Notation "x" :=
x (
in custom exp at level 0,
x ident) :
mcltt_scope.
Notation "'λ' A e" := (
a_fn A e) (
in custom exp at level 1,
A custom exp at level 0,
e custom exp at level 60) :
mcltt_scope.
Notation "f x .. y" := (
a_app .. (
a_app f x) ..
y) (
in custom exp at level 40,
f custom exp,
x custom exp at next level,
y custom exp at next level) :
mcltt_scope.
@@ -294,7 +294,7 @@
Mcltt.Core.Syntactic.Syntax
Notation "n{{{ x }}}" :=
x (
at level 0,
x custom nf at level 99,
format "'n{{{' x '}}}'") :
mcltt_scope.
Notation "( x )" :=
x (
in custom nf at level 0,
x custom nf at level 60) :
mcltt_scope.
-
Notation "~ x" :=
x (
in custom nf at level 0,
x constr at level 0) :
mcltt_scope.
+
Notation "'^' x" :=
x (
in custom nf at level 0,
x constr at level 0) :
mcltt_scope.
Notation "x" :=
x (
in custom nf at level 0,
x ident) :
mcltt_scope.
Notation "'λ' A e" := (
nf_fn A e) (
in custom nf at level 2,
A custom nf at level 1,
e custom nf at level 60) :
mcltt_scope.
Notation "f x .. y" := (
ne_app .. (
ne_app f x) ..
y) (
in custom nf at level 40,
f custom nf,
x custom nf at next level,
y custom nf at next level) :
mcltt_scope.
diff --git a/ext/prop-eq/Mcltt.Core.Syntactic.System.Tactics.html b/ext/prop-eq/Mcltt.Core.Syntactic.System.Tactics.html
index 8c8bd88..8ee7b5a 100644
--- a/ext/prop-eq/Mcltt.Core.Syntactic.System.Tactics.html
+++ b/ext/prop-eq/Mcltt.Core.Syntactic.System.Tactics.html
@@ -37,10 +37,10 @@
Mcltt.Core.Syntactic.System.Tactics
#[
global]
Ltac pi_univ_level_tac :=
match goal with
- | |-
{{ ~_ ⊢s ~_ : ~_ }} =>
mauto 4
- |
H :
{{ ~?
Δ ⊢ ~?
A : Type@?
j }} |-
{{ ~?
Δ , ~?
A ⊢ ~?
B : Type@?
i }} =>
+ | |-
{{ ^_ ⊢s ^_ : ^_ }} =>
mauto 4
+ |
H :
{{ ^?
Δ ⊢ ^?
A : Type@?
j }} |-
{{ ^?
Δ , ^?
A ⊢ ^?
B : Type@?
i }} =>
eapply lift_exp_max_right;
mauto 4
- | |-
{{ ~?
Δ ⊢ ~?
A : Type@?
j }} =>
+ | |-
{{ ^?
Δ ⊢ ^?
A : Type@?
j }} =>
eapply lift_exp_max_left;
mauto 4
end.
@@ -52,7 +52,7 @@
Mcltt.Core.Syntactic.System.Tactics
#[
local]
Ltac invert_wf_ctx1 H :=
match type of H with
- |
{{ ⊢ ~_ , ~_ }} =>
+ |
{{ ⊢ ^_ , ^_ }} =>
let H' :=
fresh "H"
in
pose proof H as H';
progressive_invert H'
diff --git a/ext/prop-eq/indexpage.html b/ext/prop-eq/indexpage.html
index cb8aee4..6afcb1d 100644
--- a/ext/prop-eq/indexpage.html
+++ b/ext/prop-eq/indexpage.html
@@ -681,7 +681,7 @@
Global Index
nf:_ _ .. _ (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
nf:λ _ _ (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
nf:_ (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
-
nf:~ _ (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
+
nf:^ _ (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
nf:( _ ) (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
n{{{ _ }}} (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
exp:_ , _ (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
@@ -704,7 +704,7 @@
Global Index
exp:_ _ .. _ (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
exp:λ _ _ (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
exp:_ (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
-
exp:~ _ (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
+
exp:^ _ (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
exp:( _ ) (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
exp:_ [ _ ] (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
{{{ _ }}} (mcltt_scope) [notation, in
Mcltt.Core.Syntactic.Syntax]
@@ -928,7 +928,7 @@
Notation Index
nf:_ _ .. _ (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
nf:λ _ _ (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
nf:_ (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
-
nf:~ _ (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
+
nf:^ _ (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
nf:( _ ) (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
n{{{ _ }}} (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
exp:_ , _ (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
@@ -951,7 +951,7 @@
Notation Index
exp:_ _ .. _ (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
exp:λ _ _ (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
exp:_ (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
-
exp:~ _ (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
+
exp:^ _ (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
exp:( _ ) (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
exp:_ [ _ ] (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]
{{{ _ }}} (mcltt_scope) [in
Mcltt.Core.Syntactic.Syntax]