Cella 語言參考

這份文件說明 Cella 的每一種寫法：怎麼寫、是什麼意思。可以在 cella-lang.org 直接試。

文中每個 cella 程式區塊都是一個完整、可以檢查的檔案。

1. 檔案與模組

一個檔案是一個模組。檔頭寫要用的模組，之後是宣告。

import std
import io
import string

def main : IO Unit := putStr "hello"

• import M：用模組 M 的公開定義。
• import M as N：以 N.名字 取用。
• import M (a, b)：只取 a、b。
• import 只能寫在第一條宣告之前。
• 模組名可以帶點，點就是目錄：
  • import util.math 是入口旁的 util/math.cella；
  • import cpp.int 是套件 cpp 的子模組 packages/cpp/src/int.cella。
• 函式庫（標準庫與套件）的定義，名字只由 namespace 決定，與在哪個檔無關：cpp.int 裡 namespace cpp 下的 add 叫 cpp.add。程式的定義帶模組名（util.math.m）。
• 常用的模組：std（自然數、布林、串列、路徑等基礎）、io（輸入輸出與 IO）、string（字串運算）、int（整數）、notation（+ 等中綴記號）。

2. 詞法

符號以 ASCII 為主，每個都有好打的寫法；Unicode 寫法是別名：->（→）、<-（←）、*（×）、Path a b（a ≡ b）、/\（∧）、\/（∨）。錯誤訊息與 Inspect 預設也印 ASCII（命令列加 --unicode、瀏覽器呼叫 set_unicode_output(true) 改印 Unicode）。

2.1 註解

import std
-- 單行註解
/- 區塊註解，
   /- 可以巢狀 -/ -/
/-- 文件註解：附在下一條宣告上 -/
def one : Nat := 1

2.2 名字

• 由字母（含中文、希臘字母等 Unicode 字母）或 _ 開頭，之後可以接字母、數字、_、'：x、x'、α₁、succ_lemma。
• 限定名用 . 串接：Nat.add、p.x。
• 單獨的 _ 是洞（讓 Cella 推出來的部分），不是名字。
• 跳脫：r#名字 是名字叫「名字」的識別字，名字可以是關鍵字或 _：def r#in (r#data : Nat) : Nat := r#data、fun (r#_ : Nat) => r#_。點後面那一段可以直接是關鍵字：v.end、Vector.end（在 namespace 裡定義時寫 def r#end）。訊息裡名字是關鍵字的印成 r#名字。關鍵字清單見附錄。

2.3 數字

十進位的自然數：0、42、18446744073709551616（大數也可以）。負數 -3 的 - 要緊貼數字。

2.4 字串

import std
import string

def plain : String := "一般字串，跳脫 \n \t \" \\"
def name : String := "Cella"
def greeting : String := f"hello, {name}! {{大括號本身}}"
def poem : String := """
  第一行
  第二行
  """
def raw : String := r"""
  printf("%d\n", x);
  """

• "…"：一般字串，不能跨行；跳脫只有 \n \t \r \" \\。
• f"…{e}…"：字串內插。{e} 裡的運算式經 ToString 轉成字串；{{、}} 是大括號本身。
• """…"""：多行字串。縮排以結尾 """ 的欄位為準去掉；開頭 """ 之後的換行不算。
• f"""…"""：可以內插的多行字串。
• r"""…"""、fr"""…"""：反斜線不跳脫（適合內嵌別的語言的原始碼）。

3. 宣告

每種宣告都以關鍵字開頭，後面接名字、參數、型別。

3.1 def 與 theorem

import std

def double (n : Nat) : Nat := add n n

theorem doubleZero : double 0 ≡ 0 := refl

• def 名字 參數… : 型別 := 本體。型別一定要寫。
• theorem 與 def 寫法相同，用在證明。
• 本體之後可以接 where 子句，定義只在這條定義裡用的輔助定義（見下）。

data Nat = zero | succ Nat
data Bool = true | false

def isEven (n : Nat) : Bool := ev n
  where
    ev (k : Nat) : Bool := match k with
      | zero => true
      | succ j => od j
    od (k : Nat) : Bool := match k with
      | zero => false
      | succ j => ev j

def count (start : Nat) (n : Nat) : Nat := go n
  where go (k : Nat) : Nat := match k with
    | zero => start
    | succ j => succ (go j)

• where 子句：名字 參數… : 型別 := 本體。子句的名字從行首開始時，同一欄的下一個名字是下一個子句；與 where 寫在同一行時以 ; 分隔。子句之後可以再接自己的 where。
• 子句可以遞迴、互相呼叫，也可以呼叫外面的定義；可以用外面定義的參數（count 的 start）。
• 子句是一條獨立的頂層定義 外層名字.子句名字（count.go），參數是它用到的外層參數加上自己的參數；終止性和一般的定義一樣檢查。沒寫型別的子句只能是非遞迴的。

用量度證明終止

遞迴定義預設要結構遞減（在參數的子項上遞迴；字典序、互遞迴也會自動找）。不是在子項上遞迴時，在本體之後寫 termination_by 量度：

import omega

def upto (n : Nat) (m : Nat) : Nat :=
  if Nat.blt n m then upto (succ n) m else n
termination_by sub m n

• 量度是 Nat，可以用參數。每個遞迴呼叫都要讓量度變小：呼叫處引數的量度小於目前參數的量度。
• 證明時看得到外層 if 的條件，以及 match 對參數的細化。預設以 omega 證（要 import omega），它懂加法、乘上常數、截斷減法 sub 與 pred。
• 證不出來時，錯誤指出是哪個呼叫，並列出兩邊的量度。可以在 termination_by 之後接 decreasing_by { tactics } 自己證：目標是「呼叫處的量度 < 界限」，上下文有「目前的量度 < 界限 + 1」與 if 的條件。
• 互遞迴（mutual）時每個定義都要寫量度。
• 遞迴的名字只能以「套滿明確引數的呼叫」出現：不能當成函式傳給 map，也不能在 do 或 tactic 區塊裡。
• 定義會翻成一個帶界限的版本 名字.bounded：界限從「量度 + 1」開始，每次遞迴減一，所以照常計算（refl、cella run 的三個後端都一樣），量度只在入口算一次。證明 名字 的性質時，展開它會先看到這個版本。

3.2 參數

import std

def const {A : Type} {B : Type} (a : A) (b : B) : A := a

def pick (b : Bool) (x y : Nat) : Nat := match b with
  | true => x
  | false => y

• (x : A)：一般參數；(x y : A) 一次宣告多個同型別的參數。
• {A : Type}：隱式參數，呼叫時由 Cella 推出；要明確給時寫 f {Nat} x。
• {{inst : C A}}：實例參數，由型別類別的實例解析填入。
• (0 x : A)：抹除的參數（只在型別裡用，執行時不存在）；(1 x : A)：線性參數（恰好用一次）。
• mode 可以允許其他用量：mode X extends core grades {0, omega}（omega 或 ω 是任意次），或自訂的 semiring（見型別論）。

3.3 postulate

postulate 名字 參數… : 型別：宣告一個不給定義的常數（假設）。用到它的定義，判決會列出這個假設。

extern 名字 參數… : IO (Either String 結果)：宣告一個由執行環境提供的函式（外部函式）。型別檢查把它當成 postulate；判決把它列成「外部函式」的假設（JSON 的 kind 是 external），用到它的定義，直接或間接，都帶著。

import std
import io

extern host_write (port : Nat) (level : Nat) : IO (Either String Unit)

def signal : IO (Either String Unit) := host_write 2 1

• 參數只能是 Nat 或 Bool，而且要明確寫出（不能是隱式參數）；結果一律是會失敗的 IO，結果 是 Nat、Bool 或 Unit。

• 型別後面可以寫 ensures p（p : 結果 -> Bool）：呼叫者拿到的是 IO.Ensured 結果 p，成功時帶著 p v = true 的證明，證明可以直接用。宿主回的值沒通過 p 時，程式得到 left，訊息說它違反了契約；這是執行時的檢查，不是公設。

  import std
  import io
  
  extern host_level (port : Nat) : IO (Either String Nat) ensures (fun (v : Nat) => Nat.blt v 2)

• Cella 不內建任何外部函式。哪些函式存在，由執行環境自己的套件宣告；沒有提供的環境，呼叫時拿到 left，訊息說它沒有提供，程式可以處理。

• 程式要編成 WebAssembly 元件時，外部函式以 @[wit "介面" "簽名"] 寫出它在 WIT 介面裡的位置，定義以 @[wit "run: func()"] 標成元件的匯出。 WIT 的簽名是正本：參數一對一、依序，u8、u16、u32、u64 對 Nat，bool 對 Bool，string 對 String，沒有結果對 IO Unit； 不一致時拒絕，訊息指出第幾個參數。這一版只收一個介面、沒有結果的函式，匯出只收沒有參數的 IO Unit。執行時 Nat 超出 WIT 型別的寬度就中止。

  import std
  import io
  
  @[wit "cos-mos:device/device@0.1.0" "pin-write: func(pin: u8, level: bool)"]
  extern pinWrite (pin : Nat) (level : Bool) : IO Unit
  
  @[wit "run: func()"]
  def run : IO Unit := pinWrite 2 true

3.4 data（歸納型別）

import std

data Color = red | green | blue

data Tree (A : Type) = leaf | node (Tree A) A (Tree A)

def size {A : Type} (t : Tree A) : Nat := match t with
  | leaf => 0
  | node l x r => succ (add (size l) (size r))

• data 名字 參數… = 建構子 | 建構子 | …；第一個建構子前可以多寫一個 |。
• 建構子寫成 名字 引數型別…，或 名字 : 完整型別，或 名字 (x : A) … : 回傳型別。
• 帶索引的型別：data Vec (A : Type) : Nat -> Type = …。
• 結尾可以加 deriving C1, C2 自動產生定義：
  • Eq：eq_T : T -> T -> Bool。
  • Json（要 import json）：T.toJson : T -> Json 與 T.fromJson : Json -> Either String T。形狀是 {"k": 建構子名, 欄位名: 值}，欄位要有名字（c (x : A)）；Option 是 null 或值，配對是兩個元素的陣列。缺欄位、多出的欄位、不認得的建構子都是帶路徑的錯誤（$.items[0].body: missing field "c" of constructor sWhile）。mutual 裡的 data 也可以；有型別參數的 data 還不行。

import json

data Shape = circle (r : Nat) | rect (w : Nat) (h : Nat) deriving Json

def text : Json.render (Shape.toJson (rect 2 3)) = "{\"k\":\"rect\",\"w\":2,\"h\":3}" := refl
def back : Json.decode Shape.fromJson "{\"k\":\"circle\",\"r\":1}" = right (circle 1) := refl

3.5 record

import std

record Point where { x : Nat; y : Nat }

def p : Point := { x := 1, y := 2 }
def px : Nat := p.x
def q : Point := { p with y := 5 }

• record 名字 參數… where { 欄位 : 型別; … }。
• 建立：{ 欄位 := 值, … }；更新：{ r with 欄位 := 值 }；取欄位：r.欄位。
• 每個 record 是自己的型別：兩個 record 有同名的欄位也不會混淆。

3.6 class 與 instance（型別類別）

import std

class Describe (A : Type) where { describe : A -> Nat }

instance describeBool : Describe Bool where { describe := fun b => match b with | true => 1 | false => 0 }

def describeTwice {A : Type} {{d : Describe A}} (a : A) : Nat := add (describe a) (describe a)

• class 名字 參數… [extends 父類別…] where { 方法 : 型別; … }；方法可以有預設值 方法 : 型別 := 預設。
• instance 名字 參數… : 類別 型別 where { 方法 := 實作; … }，或 instance 名字 … : 類別 型別 := 值。

3.7 namespace、section、open

import std

namespace Geo
def unit : Nat := 1
end Geo

def two : Nat := add Geo.unit Geo.unit

• namespace A … end A：裡面的定義名字前面加上 A.。
• open A：之後可以直接用 A 裡的名字（同 C++ 的 using namespace A）。沒有歧義才能省略：打開的幾個 namespace（或匯入的名字）有兩個以上不同的 f 時，裸名 f 報歧義並列出候選，請寫完整名稱或點記法；自己的定義與區域變數照舊遮蔽它們。
• export open A：同 open A，而且 import 這個模組的檔也打開 A（經過 import 鏈遞移）。export 只有緊接 open 時是語法，照舊能當名字。
• section … end：把一段宣告圍起來（可以搭配 variable 宣告共用的參數）。

3.8 屬性與選項

• @[simp]、@[reducible]、@[irreducible] 等寫在宣告前，一個 @[…] 放一個屬性。
• set_option maxHeartbeats N in 寫在宣告前，放寬這條定義的檢查預算。
• private：只在這個模組裡看得到。

3.9 記號宣告

• infixl 65 "+" := add、infixr、prefix、postfix：宣告中綴、前綴、後綴運算子與優先序（數字越大越緊）。
• notation：多段的記號。運算子要在宣告之後（或 import 了宣告它的模組之後）才能用。
• 運算子由這些字元組成：+ ! # $ % & ~ \ ^ < > 與數學符號（⊕ ⊗ ≤ ≥ ≐ ≠ ≈ ∘ ⋅ 等）。<-、->、=>、|> 是內建的符號，不是運算子；==、<=、=? 是兩個字元的運算子。

3.10 模態

data B = tt | ff

modality secret : core -> core

def hide : secret.Type B := secret.mk tt

def keep (@secret b : B) : secret.Type B := secret.mk b

def apply (f : (@secret x : B) -> secret.Type B) (s : secret.Type B) : secret.Type B :=
  let secret.mk x := s in f x

• modality mu : m -> n：宣告模態（從 mode m 到 mode n）；mu.Type A 是模態型別（Unicode 寫法 ⟨mu | A⟩）。
• mu.mk a：放進模態——a 在鎖 mu 之下檢查：外面沒有標註的變數不能用。let mu.mk x := s in ...：拆開，x 帶標註 mu，只能在鎖 mu 之下用。
• (@mu x : A)：參數帶模態標註；(@mu x : A) -> B 是模態函式型別，套用時引數在鎖 mu 之下檢查。模態不同的函式型別不相同。
• law mu nu = rho：鎖的合成（並排就是合成，外層在前；Unicode 寫法 mu ∘ nu）；law mu => nu：標註 mu 的變數可以用在鎖 nu 之下（nu 可以是 id）。law 的左邊至少兩個模態，而且要合流（重疊的 law 從兩邊化簡要得到同一個結果，宣告時檢查）。
• 鎖由 elaborator 與獨立的檢查器各自檢查。規則見 typing-rules 第 10 章。

3.11 codata（餘歸納型別）

data Nat = zero | succ Nat

codata Stream (A : Type) = head : A, tail : Stream A
codata Pair = head : Nat, other : Nat

def zeros : Stream Nat := { head => zero, tail => zeros }
def p : Pair := { head => succ zero, other => zero }

def a : Nat := head zeros
def b : Nat := head p
def c : Nat := Pair.head p
def d : Nat := zeros.tail.head

• codata 名字 參數… = 投影 : 型別, …：以「能觀察到什麼」定義的型別（可以無窮）；用 { 投影 => 值, … } 建立。
• 遞迴必須在 { … } 之內（有守衛），而且不能被觀察：{ head => head s, … } 這種回頭讀自己的寫法會被拒絕。
• 投影在型別的命名空間裡：Pair.head 永遠指那個型別的投影；s.head 依 s 的型別找。兩個 codata 有同名的投影時，head x 依 x 的型別選；不套用的 head（例如當作函式傳出去）指最後宣告的那個，兩個匯入都提供時要寫限定名。

3.12 SProp（定義上的證明無關）

data N = zero | succ N
data STrue : SProp = sI
data SEmpty : SProp =
data SAnd (P Q : SProp) : SProp = sand P Q

def swap (P Q : SProp) (x : SAnd P Q) : SAnd Q P := match x with
  | sand p q => sand q p

def absurdS (A : Type) (e : SEmpty) : A := match e with

def irr (P : SProp) (F : P -> Type) (p q : P) (x : F p) : F q := x

• SProp（SProp 1、SProp l）是命題的 sort：型別在 SProp 的任兩個值定義上相等（上面的 irr 不用證明就成立）。
• SProp l : Type (l+1)；值域在 SProp 的函式型別在 SProp；量化 Type 的命題在 SProp 1（直謂）。SProp 不能當 Type 用。
• data 名字 … : SProp = …：宣告在 SProp 的型別。它只能 match 出另一個證明（型別在 SProp）；沒有建構子的型別例外，可以消去到任何型別。不能有路徑建構子。
• 路徑型別與 Glue 只在 Type 裡（證明之間本來就相等）。
• SProp 在運算式裡是 sort；要當名字用寫 r#SProp。

4. 運算式

4.1 套用與運算子

• 函式套用是並排：f x y（先 f x，再套用 y）。
• 點記法：e.f 在 e 的型別是 T、有 T.f 時就是 T.f e（e 是 T.f 的第一個明確參數）：c.get、(c.bump 2).get。record 的欄位照舊優先。
• 內建的運算子，由鬆到緊：
  • A -> B（函式型別，右結合）
  • a = b（相等，import identity）、a ≡ b（路徑；ASCII 寫 Path a b），兩者同一層、不結合
  • A × B（積型別，右結合）
  • a - b、i /\ j、i \/ j（區間的交與聯；∧、∨ 是別名）
  • x |> f a（管線：等於 f a x）
  • 使用者宣告的運算子（例如 import notation 之後的 a + b、布林比較 a == b）
  • 套用（最緊）
• @f：明確套用，所有隱式參數都要自己給。

4.2 型別

• Type、Type 1：型別的型別（宇宙）。不帶層級的 Type 就是 Type 0；要推斷層級寫 Type _。
• (x : A) -> B x：依值函式型別；{x : A} -> B：隱式參數的函式型別。
• (x : A) × B x：依值配對型別。

4.3 fun

import std

def inc : Nat -> Nat := fun n => succ n
def add3 : Nat -> Nat -> Nat -> Nat := fun a b c => add a (add b c)
def swap : Pair Nat Nat -> Pair Nat Nat := fun (a, b) => mkPair b a

• fun x => e；參數可以帶型別 fun (x : A) => e、隱式 fun {A} => e。
• fun (a, b) => e：直接拆開 Pair（mkPair a b）；可以巢狀 fun (i, (c, r)) => …。

4.4 let

import std

def area (w : Nat) (h : Nat) : Nat :=
  let s := mul w h
  add s s

def inline : Nat := let x := 2 in mul x x

• let x := v in e；in 可以省略：let 在行首時，下一行（和 let 同欄）就是本體。
• 可以標型別：let x : Nat := v。

4.5 if

if 條件 then 運算式 else 運算式。在運算式裡兩個分支都要寫；條件是 Bool。

4.6 match

import std

def describe (n : Nat) : Nat := match n with
  | zero => 0
  | succ zero => 1
  | succ (succ k) => match k with
    | zero => 2
    | succ j => 3

• match e with | 樣式 => 運算式 | …。
• 分支的歸屬由縮排決定：縮排更深的 | 屬於內層的 match，所以巢狀的 match 不用加括號。
• 樣式：名字（綁定）、_、建構子加子樣式（succ (succ k)）、配對 (a, b)、串列 [x, y]、()（不可能的情形，沒有 =>）、.x（由型別決定的 dot 樣式）。
• 同時對多個運算式：match (a, b) with | (true, x) => … | (false, _) => …——每一欄照建構子分情形，變數與 _ 承接其餘，沒有承接的組合報 non-exhaustive（Lean 的 match a, b with）。
• 對運算式 match 時（不只是變數），運算式在每個分支裡被換成那個建構子：目標裡出現的、以及型別依賴它的假設都跟著細化。with (e) | … 是同一件事的另一種寫法（Agda 的 with）；巢狀的 with 照縮排分屬內外層。

data Nat = zero | succ Nat
data Bool = true | false

def isZero (n : Nat) : Bool := match n with
  | zero => true
  | succ k => false

def the (A : Type) (a : A) : A := a

def onlyZero (n : Nat) (h : isZero n ≡ true) : Nat := with (isZero n)
  | true => n
  | false => let wrong := the (false ≡ true) h in zero

4.7 字面量與其他

• 元組：(a, b)；(a, b, c) 是 (a, (b, c))。期望型別是 Pair A B（或其他只有一個建構子、兩個欄位的型別）時，(a, b) 就是那個建構子（mkPair a b）；其他時候是依值配對 A × B，取用 fst p、snd p。兩種都可以用元組樣式 (a, b) 拆開（fun、for、match）。

import std
def scores : List (Pair Nat Nat) := [(1, 90), (2, 85)]
def total : Nat := scores |> map (fun (id, s) => s) |> foldr add 0
def t : total ≡ 175 := refl

• 串列：[1, 2, 3]（可以有結尾逗號）。
• 型別標註：(e : T)。
• 洞：_（讓 Cella 推）、? 或 ?名字（留下待填的洞，檢查結果會列出它的型別）。

5. do：寫會跑的程式

import std
import io
import string

def countdown (n : Nat) : IO Unit := do
  let mut k := n
  for i in [1, 2, 3] do
    putStr f"step {i}"
    k := succ k
  if Nat.ble k 10 then
    putNat k
  else
    putStr "big"

def main : IO Unit := countdown 3

do 區塊裡一行一個敘述，由縮排決定區塊的範圍（同一欄是下一個敘述，更深的行是同一個敘述的延續）。也可以用 do { 敘述; 敘述 } 寫在一行。

敘述	意思
x <- e	執行動作 e，結果叫 x
_ <- e	執行動作 e，丟掉結果
let x := v	純粹的值取名字
let mut x := v、x := v	可變變數與指定
for x in xs do 區塊	對串列的每個元素做一次；ys <- for … 把每次的結果收成串列
if c then 區塊 else 區塊	else 可以省略；else if 可以串接
match e with | p => 區塊	分支是敘述區塊
break、continue、return e	跳出迴圈、下一圈、提前回傳
e	執行動作；最後一個敘述的值是整個 do 的值

在敘述裡還可以寫：

• (<- e)：在運算式中間執行動作 e，取它的結果（由左到右執行）：putNat (add (<- readNat) 1)。
• e?：e 是 IO (Either E A) 時，失敗就讓整個 do 回傳那個失敗。
• await t：等任務 t 完成並取出結果；任務由 async e 或 spawnTask job 建立。

import std
import io

def main : IO Unit := do
  t <- async (pure 21)
  putNat (mul (await t) 2)

5.1 其他 monad 的 do

do 不只用在 IO：預期型別是 M A、M 有 Monad 的 instance 時，x <- e 是 bind e (fun x => …)，最後一句是整個區塊的值。let mut、for、break、return 一樣能用。

• Monad（import std）：方法 pure : {A : Type} -> A -> M A、bind : {A : Type} -> {B : Type} -> M A -> (A -> M B) -> M B。
• Option、Either E、List 已有 instance；IO 的 instance 在 io，它的 pure、bind 是 IO 的原語 IO.pure、IO.bind。
• 預期型別是 IO 時，pure、bind 直接是 IO 的原語。
• 自己的型別寫 instance 時，方法開頭的型別參數可以不接（pure := fun a => good a），也可以明寫（pure := fun A a => good a）。

import std

data Chk (A : Type) = good A | fail String

instance monadChk : Monad Chk where { pure := fun a => good a; bind := fun m f => match m with | good a => f a | fail w => fail w }

def both : Chk Nat := do
  a <- good 1
  b <- good 2
  pure (add a b)

找不到 instance 時，錯誤會說是哪個型別：「no instance of Monad Box was found」。

5.2 以模式綁定：模式 <- e

<- 的左邊可以是模式：只有一個建構子的型別（或 tuple）直接拆開；可能比對失敗的模式寫 | 替代，比對不到時改做替代。沒寫替代、模式又可能失敗時，錯誤指出缺了哪個建構子（不會像 Haskell 的 MonadFail 那樣把失敗藏進 monad）。

import std

data Two = two (a : Nat) (b : Nat)

def pairOf (n : Nat) : Option Two := some (two n (succ n))

def sum3 : Option Nat := do
  two a b <- pairOf 3
  pure (add a b)

def firstOr (xs : List Nat) : Option Nat := do
  cons x rest <- some xs | pure 0
  pure x

區塊剩下的敘述就是比對成功之後要做的事。大括號的寫法一樣可以用：do { two a b <- pairOf 3; pure (add a b) }。

6. 證明

6.1 路徑與相等

• a = b 是 a 與 b 相等的證明的型別（Eq _ a b；import std 或 import identity）：只用 data 與 match，不需要 cubical。refl 證明 a = a，計算後相等的也接受。操作在 Eq 底下，證明在前，可以用點記法：h.sym、h.trans k、h.cong f、h.subst P x、Eq.transport h x；建構子寫 Eq.refl（refl 依期望型別選）。
• Path a b（Unicode 寫 a ≡ b；內建，不需要匯入）是 a 到 b 的路徑型別（cubical 的相等，univalence、HIT 靠它）；refl 也證明 Path a a（寫成 Path.refl；refl 依期望型別選 Eq.refl 或 Path.refl）。Eq.toPath／Path.toEq（import identity.paths）在兩者之間互轉。
• 建構子屬於型別的 namespace：T.c 是型別 T 的建構子 c（Nat.succ、Bool.true、Eq.refl）；不會混淆時照舊直接寫 succ。
• a == b 是布林比較（import notation），結果是 Bool，不是證明。ordering.relations 的順序關係寫成 a <= b、a < b，兩者相等的命題寫 a =? b；乘法沒有中綴記號（* 是積型別，寫 mul a b）。
• 路徑是區間上的函式：fun i => …，p i 取路徑上的點。
• transport、transp、hcomp、Glue、ua 等是 cubical 型別論的原語（ua 把型別等價變成路徑）。

import std
import identity

def addZeroId : add 2 0 = 2 := refl

def addZero : add 2 0 ≡ 2 := refl

def symm {A : Type} {a : A} {b : A} (p : a ≡ b) : b ≡ a := fun i => p (1 - i)

6.2 tactic

by { … } 裡用 tactic 一步一步建構證明，步驟之間用換行或 ; 分開：

import std

theorem andComm (a : Bool) (b : Bool) : and a b ≡ and b a := by {
  cases a
  cases b
  rfl
  rfl
  cases b
  rfl
  rfl
}

常用的 tactic：intro、exact e、apply e、rfl、rewrite e、cases x、induction x、simp、ring、omega、linarith、decide、have x : T := e、constructor、left、right、exfalso、contradiction、try t、repeat t、first | t | t。

6.3 calc

calc a ≡ b by p; b ≡ c by q 把一連串的相等串起來。

7. 版面規則摘要

• 頂層的宣告以關鍵字開頭，換行沒有特別的意義。
• do 區塊、do 裡 if／for／match 的分支區塊、match 的分支、行首的 let 以縮排決定範圍：
  • 和區塊同一欄的行：下一個敘述（或分支）；
  • 縮排更深的行：同一個敘述的延續；
  • 縮排更淺的行：區塊結束。
• 括號 ( )、[ ]、{ } 裡面暫停版面規則。

7.1 格式化：cella fmt

• cella fmt 檔案… 就地格式化；cella fmt --check 檔案… 不改檔，有要改的就列出並以非零結束。
• 只動空白，記號（含註解、語法糖）照原文：同一行的多個空白收成一個，連續空行最多一行，縮排正規化成每層兩格（相等的縮排仍相等、較深的仍較深）。
• 超過 100 字的行依序在這些地方換行：match 分支的 | 之前、:= 之後、then／else 之前、=> 之後、, 之後、-> 之後、型別的 : 之前，最後是套用的引數（一個一行）；括號裡遞迴，每深一層多縮兩格。含 do、by、where、calc 的行不拆。
• 格式化前後剖析出的語法樹要相同；某條定義會變的話，那條定義保留原樣並提示。

附錄：關鍵字

要把這些字當名字用，寫成 r#名字（點後面那一段不必）。瀏覽器的 keywords() 給同一份清單。

• 硬關鍵字（任何位置）：Glue、Level、PathP、Size、Type、builtin、calc、class、codata、data、declare_syntax_cat、def、do、elab、else、end、extern、fst、fun、glue、hcomp、if、import、in、inductive、inf、infixl、infixr、instance、let、lmax、lsuc、lzero、macro_rules、match、mutual、namespace、notation、open、postfix、postulate、prefix、private、record、rule、section、set_option、snd、structure、syntax、tactic、then、theorem、transp、transport、ua、unglue、variable、where、with
• 上下文關鍵字（只在特定位置）：by、deriving、termination_by、decreasing_by、local、scoped、ensures
• 保留字（給 mode 與模態）：mode、modality、law、grades