Agda 練習 - zyxwvの日記
あまりわかってないけど、とりあえずいくつか適当な関数を書いたのでメモ。依存型うける(気がする)。 agda2 の emacs モードが使いこなせないのと関数を実行する方法がわからんのが問題である。 module NList where data Nat : Set where zero : Nat succ : Nat -> Nat _+_ : Nat -> Nat -> Nat zero + n = n (succ m) + n = succ (m + n) _*_ : Nat -> Nat -> Nat zero * _ = zero (succ zero) * n = n (succ m) * n = m + (m * n) data List (A : Set) : Nat -> Set where [] : List A zero _::_ : {n : Nat} -> A ->
Lambda Tamer
The Lambda Tamer project tackles the issues surrounding computer formalization of programming languages and their tools, based around the Coq proof assistant. The Lambda Tamer methodology centers on higher-order and dependently-typed abstract syntax and aggressive automation. The main project output is a library of Coq definitions, theorems, and tactics in support of building certified compilers f
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
http://www.sato.kuis.kyoto-u.ac.jp/~igarashi/CoPL/
