Agda言語

Agda言語

Agda言語とは？

• Agda言語は、いわゆる函数型プログラミング言語です。

• Agda言語で、論理式やその証明を記すこともできます。

  • • Agda言語は「強い型付」を持つ言語です。しかも、その型システムは「依存型」と言われるものを含むため、型を述語、その型の要素を述語の証明と見なすことができます（いわゆる型としての論理式、formulae as types）

• • 詳しい情報が Agda wiki にあります。