blog: syntax highlight the operator blog

.vscode/ltex.dictionary.en-US.txt

@@ -5,3 +5,12 @@ VSCode
 unqualify
 extensionality
 impredicative
+HOAS
+Coq
+metavariables
+desugar
+unfoldable
+codomain
+Bruijn
+Agda
+mixfix

aya/blog/binops.aya.md

@@ -0,0 +1,62 @@
+# Binary operators in Aya
+
+We have designed a binary operator system in Aya which happens to be (we didn't copy!) very similar to
+[Rhombus](https://plt.cs.northwestern.edu/pkg-build/doc/enforest/Operator_Precedence_and_Associativity.html) (a.k.a. Racket 2)
+and [Swift 5.7](https://docs.swift.org/swift-book/ReferenceManual/Declarations.html#ID550).
+
+TL;DR: it supports making _any_ identifier a custom operator
+with precedences specified by a partial ordering.
+Left and right associativities are supported in addition to that.
+
+The precedence and associativity information is bound to a
+name, not a definition. This means we can import a name from
+another module with changes to its name, associativity, and precedence.
+Importing with renaming is an established feature, but changing associativity
+and precedence is not that popular (though implemented in Agda already).
+
+```aya-hidden
+inductive Nat
+```
+
+Here are some code examples (implementations are omitted for simplicity):
+
+```aya
+// Left-associative
+def infixl + (x y : Nat) : Nat => {??}
+// Left-associative, bind tighter than +
+def infixl * (x y : Nat) : Nat => {??} tighter +
+// Prefix operator
+def fixl ! (x : Nat) : Nat => {??}
+// Postfix operator
+def fixr ? (x : Nat) : Nat => {??}
+```
+
+The `tighter` keyword works like this: when there are expressions like
+`a * b + c` which may either mean `(a * b) + c` or `a * (b + c)`,
+we will put the tighter operator in the parenthesis.
+In case we found the two operators share the same priority, Aya will report an error.
+
+When importing operators from other modules,
+we can locally specify additional associativity and precedence information:
+
+```
+open import Primitives using (
+  invol       as fixl  ~  tighter =, \/, /\,
+  intervalMin as infix /\ tighter \/,
+  intervalMax as infix \/,
+)
+```
+
+This should allow fine-grained control over the precedence and associativity of operators.
+In case there is a cycle in the graph of operator precedence, Aya will report an error.
+
+Specifying precedence of operators with a partial ordering is way better than with a number.
+In Haskell, if we already have `infix 3 +` and `infix 4 *`, and we hope to add a new operator
+which has higher precedence than `+` but lower than `*`, it's going to be impossible.
+Agda introduced [float-point precedence](https://github.com/agda/agda/issues/3991)
+levels to address the issue, but I think it does not solve the essential problem:
+that I have to lookup the numbers (of existing operator precedences)
+every time I write a new operator.
+
+In the future, we plan to support mixfix operators as in Agda
+(the current framework can support mixfix easily, but abusing mixfix notations can harm readability).

aya/blog/jit-compile.aya.md

@@ -168,7 +168,7 @@ Both papers can be found in [related papers](/guide/readings).
 
 Aya reuses JVM, a highly optimized VM with two JIT compilers that produce machine code,
 and has HOAS built-in to the core language, so there is no need of reading back -- the result of compilation is directly used in our core
-language rather than a separately defined language. This also makes it less errorprone because a bug in the compiled code is
+language rather than a separately defined language. This also makes it less error-prone because a bug in the compiled code is
 a bug in the core language, which is well-understood and well-tested.
 But then the correctness (mainly type safety) of the core language relies on the correctness of the JJH compiler,
 which we do not intend to formally verify, but we believe (with reasonable confidence due to the amount of testing) that it is correct.

aya/blog/tt-in-tt-qiit.aya.md

@@ -61,11 +61,13 @@ open inductive Ty (Γ : Con) : Type
 The `ext`{} operator corresponds to the ↑ operator in the paper:
 
 ```aya
-def ext {Γ Δ : Con} (δ : Γ << Δ) (A : Ty Δ) : Γ ▷ Subst A δ << Δ ▷ A =>
+variable Γ Δ : Con
+def ext (δ : Γ << Δ) (A : Ty Δ) : Γ ▷ Subst A δ << Δ ▷ A =>
   δ ∘ π₁ (id refl) ∷ transport (Tm _) SubAss (π₂ (id refl))
 ```
 
-An instance of the type `Ty Γ` corresponds to the $A$ in the judgment $Γ⊢A~\text{type}$. The constructor `U`{} corresponds to the following rule:
+An instance of the type `Ty Γ`{} corresponds to the $A$ in the judgment $Γ⊢A~\text{type}$.
+The constructor `U`{} corresponds to the following rule:
 
 $$
 \cfrac{}{Γ⊢\mathcal{U}~\text{type}}
@@ -101,7 +103,7 @@ open inductive infix << (Γ : Con) (Δ : Con) : Type
 | _, • => εη {δ : Γ << •} : δ = ε
 ```
 
-An instance of type `Γ << Δ` corresponds to the $σ$ in the substitution typing $Γ ⊢ σ : Δ$.
+An instance of type `Γ << Δ`{} corresponds to the $σ$ in the substitution typing $Γ ⊢ σ : Δ$.
 
 ## Terms
 

package.json

@@ -1,7 +1,7 @@
 {
   "name": "aya-prover-docs",
   "version": "1.0.0",
-  "packageManager": "pnpm@9.14.4",
+  "packageManager": "pnpm@9.15.0",
   "description": "The documentation site of the Aya prover.",
   "main": "index.js",
   "scripts": {