Example. 初步實驗的效果 [violet-0000]

目前是用 violet weave 從一個 .vt.scrbl 編譯。程式碼區塊由 violet 前處理：@vt|{…}| 的內容會被抽出、型別檢查，轉成帶標記的 HTML。其餘內容原樣交給 tr-notes

把游標移到 identifiers 上時可以看到型別；調用部分連結到它的定義；?here 這樣的 goal 會顯示 context 與 target

\universe US U

\let id(A : universe U) -> (_ : A) -> A (Auniverse U : Uuniverse S U) : Auniverse U -> Auniverse U \where
  <= \intro
  | id A xA => xA

\let ex(A : universe U) -> (_ : A) -> A (Auniverse U : Uuniverse S U) : Auniverse U -> Auniverse U \where
  <= \intro
  | ex A xA => id(A : universe U) -> (_ : A) -> A Auniverse U xA

\let open-goal(A : universe U) -> (_ : A) -> A (Auniverse U : Uuniverse S U) : Auniverse U -> Auniverse U \where
  <= \intro
  | open-goal A xA => ?hereA : universe U
x : A
⊢ A

id 定義，ex 內用到了 id，open-goal 留了一個 ?here goal。