關於本專案#
關於這個版本#
這是 Let’s play Agda 的靜態重建版。Let’s play Agda 是由 Ingo Blechschmidt （安特衛普大學 University of Antwerp）為 2025 年在帕多瓦大學開設、 由 Milly Maietti 籌辦的課程所製作的互動式 Agda 教學； 請參閱原始網站與原始儲存庫。 教學的文字與 Agda 程式碼，是原作者與下列貢獻者的作品，以 CC BY-SA 授權提供。這個版本把它們呈現為一個靜態網站，其中的 Agda 編輯器直接在你的瀏覽器裡執行 （這個版本的原始碼）。 下面描述本網站技術的章節已針對這個版本更新；致謝名單則沿用原版。
致謝#
多年來，本課程的結構與內容，受到下列活動參與者的回饋所塑造，並從中獲益良多：
- Chaos Communication Congress （2018、 2019、 2023、 2024），
- Curry Club Augsburg （2019、2021），
- 兩場 Dagstuhl 研討會 （2021、 2024），
- 2022 年 ALGAR 暑期學校，
- Proof and Computation 秋季學校 （2022、 2023、 2024），
- 維洛納大學（University of Verona）的兩門短期課程 （2022、 2024）
——特別是帕多瓦大學的學生們 （2020、 2021、 2022、 2023、 2024、 2025、 2026）。本課程的起點，是 Martín Escardó 在 2018 年的 Proof and Computation 開設的一門課，我就是在那裡學會 Agda 的， 過程中得到 Anja Petković Komel，以及後來 Matthias Ritter 的幫助。
以下人士提供了 pull request：
- Taylor Belcher
- Matteo Cusin
- @joha2
- Maja Kądziołka
這些貢獻大幅改善了本課程的呈現方式。此外，下列人士的回饋也影響深遠，我們非常感謝：
- Timur Aminev
- Martin Ceresa
- Fredrik Nordvall Forsberg
- Johannes Hartung
- Jacopo Piccione
- Alessandro Rizzi
- Noon van der Silk
開源的相依專案#
這個互動式 Agda 教學，建立在許多出色的自由軟體專案之上：
- Agda 本身，多虧 Agda Web 專案 與 Agda Language Server，它能以 WebAssembly 的形式在你的瀏覽器中執行，
- Visual Studio Code for the Web（Code - OSS），
- Ting-Gian Lua 的 agda-mode for VS Code， 以及 Andy Pan 的 ALS WASM Loader，
- cubical library。
按這裡可以看到彩帶動畫。
其他語言的類似專案#
在本機使用#
如果你偏好使用本機安裝的 Agda，我們提供了所有 Agda 程式碼的壓縮檔。
這個教學是一個靜態網站；它的儲存庫 包含了自行建置與架設所需的一切。
備份你的資料#
本專案中互動式的 Agda 元件都在你的瀏覽器裡執行。沒有任何伺服器參與， 你的 Agda 程式碼不會離開你的電腦。
你對 Agda 習題的解答，儲存在瀏覽器的 local storage 中。這個儲存空間原則上是永久的， 但實際上很容易被清除，例如在瀏覽器的私密模式下使用，或是刪除網站的「應用程式資料」時。 因此你可能會想定期下載你的解答以便保存。
你可以點這裡匯入備份。 這會把備份的內容與目前的 local storage 合併。
連續紀錄（Streak）#
當你開始填寫第一個 hole 之後，導覽列下方的左下角會出現一個小日曆，讓你追蹤自己的進度。 和你的 Agda 程式碼一樣，這份活動紀錄也只儲存在瀏覽器的 local storage 中。
你有在練習的日子
你有在休息的日子
你沒有活動的日子
為了更貼近夜貓子，我們把一天定義為在凌晨 5 點結束。如果對你有用的話，我們也會計算你 連續每天都有活動的最長紀錄。在每 7 天的時間範圍內，最多兩個休息日不會中斷連續紀錄。
Unicode 符號#
Agda 社群非常愛用 Unicode，這讓我們能在記法上模仿黑板上的數學。在這個網頁上，你可以把滑鼠
移到 Agda 片段中的特殊符號上，了解該怎麼輸入它們。許多 LaTeX 指令都可以使用，例如
\alpha 會產生希臘字母 α。
以下是本課程用到的 Unicode 符號清單。