renamed Ax vdash-tick

src/plta/Lambda.lagda

@@ -977,7 +977,8 @@ infix  4  _⊢_⦂_
 
 data _⊢_⦂_ : Context → Term → Type → Set where
 
-  Ax : ∀ {Γ x A}
+  -- Axiom
+  ⊢` : ∀ {Γ x A}
     → Γ ∋ x ⦂ A
        -------------
     → Γ ⊢ ` x ⦂ A
@@ -1103,7 +1104,7 @@ Ch : Type → Type
 Ch A = (A ⇒ A) ⇒ A ⇒ A
 
 ⊢twoᶜ : ∅ ⊢ twoᶜ ⦂ Ch `ℕ
-⊢twoᶜ = ⊢ƛ (⊢ƛ (Ax ∋s · (Ax ∋s · Ax ∋z)))
+⊢twoᶜ = ⊢ƛ (⊢ƛ (⊢` ∋s · (⊢` ∋s · ⊢` ∋z)))
   where
   ∋s = S ("s" ≠ "z") Z
   ∋z = Z
@@ -1115,8 +1116,8 @@ Here are the typings corresponding to computing two plus two.
 ⊢two = ⊢suc (⊢suc ⊢zero)
 
 ⊢plus : ∅ ⊢ plus ⦂ `ℕ ⇒ `ℕ ⇒ `ℕ
-⊢plus = ⊢μ (⊢ƛ (⊢ƛ (⊢case (Ax ∋m) (Ax ∋n)
-         (⊢suc (Ax ∋+ · Ax ∋m′ · Ax ∋n′)))))
+⊢plus = ⊢μ (⊢ƛ (⊢ƛ (⊢case (⊢` ∋m) (⊢` ∋n)
+         (⊢suc (⊢` ∋+ · ⊢` ∋m′ · ⊢` ∋n′)))))
   where
   ∋+  = (S ("+" ≠ "m") (S ("+" ≠ "n") (S ("+" ≠ "m") Z)))
   ∋m  = (S ("m" ≠ "n") Z)
@@ -1136,7 +1137,7 @@ the second after "m" is bound in the successor branch of the case.
 And here are typings for the remainder of the Church example.
 \begin{code}
 ⊢plusᶜ : ∅ ⊢ plusᶜ ⦂ Ch `ℕ ⇒ Ch `ℕ ⇒ Ch `ℕ
-⊢plusᶜ = ⊢ƛ (⊢ƛ (⊢ƛ (⊢ƛ (Ax ∋m · Ax ∋s · (Ax ∋n · Ax ∋s · Ax ∋z)))))
+⊢plusᶜ = ⊢ƛ (⊢ƛ (⊢ƛ (⊢ƛ (⊢` ∋m · ⊢` ∋s · (⊢` ∋n · ⊢` ∋s · ⊢` ∋z)))))
   where
   ∋m = S ("m" ≠ "z") (S ("m" ≠ "s") (S ("m" ≠ "n") Z))
   ∋n = S ("n" ≠ "z") (S ("n" ≠ "s") Z)
@@ -1144,7 +1145,7 @@ And here are typings for the remainder of the Church example.
   ∋z = Z
 
 ⊢sucᶜ : ∅ ⊢ sucᶜ ⦂ `ℕ ⇒ `ℕ
-⊢sucᶜ = ⊢ƛ (⊢suc (Ax ∋n))
+⊢sucᶜ = ⊢ƛ (⊢suc (⊢` ∋n))
   where
   ∋n = Z
 
@@ -1182,7 +1183,7 @@ We can fill in the hole by type C-c C-r again.
 
 And again.
 
-    ⊢suc′ = ⊢ƛ (⊢suc (Ax { }3))
+    ⊢suc′ = ⊢ƛ (⊢suc (⊢` { }3))
     ?3 : ∅ , "n" ⦂ `ℕ ∋ "n" ⦂ `ℕ
 
 A further attempt with C-c C-r yields the message:
@@ -1191,7 +1192,7 @@ A further attempt with C-c C-r yields the message:
 
 We can fill in `Z` by hand. If we type C-c C-space, Agda will confirm we are done.
 
-    ⊢suc′ = ⊢ƛ (⊢suc (Ax Z))
+    ⊢suc′ = ⊢ƛ (⊢suc (⊢` Z))
 
 The entire process can be automated using Agsy, invoked with C-c C-a.
 
@@ -1233,7 +1234,7 @@ doing so requires types `A` and `B` such that `A ⇒ B ≡ A`.
 
 \begin{code}
 nope₂ : ∀ {A} → ¬ (∅ ⊢ ƛ "x" ⇒ ` "x" · ` "x" ⦂ A)
-nope₂ (⊢ƛ (Ax ∋x · Ax ∋x′))  =  contradiction (∋-injective ∋x ∋x′)
+nope₂ (⊢ƛ (⊢` ∋x · ⊢` ∋x′))  =  contradiction (∋-injective ∋x ∋x′)
   where
   contradiction : ∀ {A B} → ¬ (A ⇒ B ≡ A)
   contradiction ()

src/plta/Properties.lagda

@@ -245,7 +245,7 @@ canonical : ∀ {V A}
   → Value V
     -----------
   → Canonical V ⦂ A
-canonical (Ax ())          ()
+canonical (⊢` ())          ()
 canonical (⊢ƛ ⊢N)          V-ƛ         =  C-ƛ ⊢N
 canonical (⊢L · ⊢M)        ()
 canonical ⊢zero            V-zero      =  C-zero
@@ -337,7 +337,7 @@ progress : ∀ {M A}
   → ∅ ⊢ M ⦂ A
     ----------
   → Progress M
-progress (Ax ())
+progress (⊢` ())
 progress (⊢ƛ ⊢N)                            =  done V-ƛ
 progress (⊢L · ⊢M) with progress ⊢L
 ... | step L↦L′                             =  step (ξ-·₁ L↦L′)
@@ -547,7 +547,7 @@ rename : ∀ {Γ Δ}
         → (∀ {x A} → Γ ∋ x ⦂ A → Δ ∋ x ⦂ A)
           ----------------------------------
         → (∀ {M A} → Γ ⊢ M ⦂ A → Δ ⊢ M ⦂ A)
-rename ρ (Ax ∋w)           =  Ax (ρ ∋w)
+rename ρ (⊢` ∋w)           =  ⊢` (ρ ∋w)
 rename ρ (⊢ƛ ⊢N)           =  ⊢ƛ (rename (ext ρ) ⊢N)
 rename ρ (⊢L · ⊢M)         =  (rename ρ ⊢L) · (rename ρ ⊢M)
 rename ρ ⊢zero             =  ⊢zero
@@ -685,7 +685,7 @@ substbind : ∀ {Γ x y N V A B C}
     ---------------------------------
   → Γ , x ⦂ A ⊢ N ⟨ x ⟩[ y := V ] ⦂ C
 
-subst ⊢V (Ax ∋x)           =  substvar ⊢V ∋x
+subst ⊢V (⊢` ∋x)           =  substvar ⊢V ∋x
 subst ⊢V (⊢ƛ ⊢N)           =  ⊢ƛ (substbind ⊢V ⊢N)
 subst ⊢V (⊢L · ⊢M)         =  subst ⊢V ⊢L · subst ⊢V ⊢M
 subst ⊢V ⊢zero             =  ⊢zero
@@ -698,7 +698,7 @@ substvar {x = x} {y = y} ⊢V Z with x ≟ y
 ... | no  x≢y              =  ⊥-elim (x≢y refl)
 substvar {x = x} {y = y} ⊢V (S x≢y ∋x) with x ≟ y
 ... | yes refl             =  ⊥-elim (x≢y refl)
-... | no  _                =  Ax ∋x
+... | no  _                =  ⊢` ∋x
 
 substbind {x = x} {y = y} ⊢V ⊢N with x ≟ y
 ... | yes refl             =  drop ⊢N
@@ -723,12 +723,12 @@ subst : ∀ {Γ x N V A B}
   → Γ , x ⦂ A ⊢ N ⦂ B
     --------------------
   → Γ ⊢ N [ x := V ] ⦂ B
-subst {x = y} ⊢V (Ax {x = x} Z) with x ≟ y
+subst {x = y} ⊢V (⊢` {x = x} Z) with x ≟ y
 ... | yes refl     =  weaken ⊢V
 ... | no  x≢y      =  ⊥-elim (x≢y refl)
-subst {x = y} ⊢V (Ax {x = x} (S x≢y ∋x)) with x ≟ y
+subst {x = y} ⊢V (⊢` {x = x} (S x≢y ∋x)) with x ≟ y
 ... | yes refl     =  ⊥-elim (x≢y refl)
-... | no  _        =  Ax ∋x
+... | no  _        =  ⊢` ∋x
 subst {x = y} ⊢V (⊢ƛ {x = x} ⊢N) with x ≟ y
 ... | yes refl     =  ⊢ƛ (drop ⊢N)
 ... | no  x≢y      =  ⊢ƛ (subst ⊢V (swap x≢y ⊢N))
@@ -753,7 +753,7 @@ cases, and fixpoints, the variable `x` is an implicit parameter for
 the relevant variable.  We are going to need to get hold of both
 variables, so we use the syntax `{x = y}` to bind `y` to the
 substituted variable and the syntax `{x = x}` to bind `x` to the
-relevant variable in the patterns for `Ax`, `⊢ƛ`, `⊢case`, and `⊢μ`.
+relevant variable in the patterns for `⊢``, `⊢ƛ`, `⊢case`, and `⊢μ`.
 Using the name `y` here is consistent with the naming in the original
 definition of substitution in the previous chapter.  The proof never
 mentions the types of `x`, `y`, `V`, or `N`, so in what follows we
@@ -907,7 +907,7 @@ preserve : ∀ {M N A}
   → M ↦ N
     ----------
   → ∅ ⊢ N ⦂ A
-preserve (Ax ())
+preserve (⊢` ())
 preserve (⊢ƛ ⊢N)                 ()
 preserve (⊢L · ⊢M)               (ξ-·₁ L↦L′)     =  (preserve ⊢L L↦L′) · ⊢M
 preserve (⊢L · ⊢M)               (ξ-·₂ VL M↦M′)  =  ⊢L · (preserve ⊢M M↦M′)
@@ -1093,7 +1093,7 @@ sequence given earlier.  First, we show that the term `sucμ`
 is well-typed.
 \begin{code}
 ⊢sucμ : ∅ ⊢ μ "x" ⇒ `suc ` "x" ⦂ `ℕ
-⊢sucμ = ⊢μ (⊢suc (Ax ∋x))
+⊢sucμ = ⊢μ (⊢suc (⊢` ∋x))
   where
   ∋x = Z
 \end{code}