Agda 中通常使用大括号 {} 表示记录类型或记录值,使用小括号 () 表示函数应用,使用方括号 [] 表示列表类型或列表值。同时,冒号 : 用作类型注释或函数类型声明。
以下是一些示例:
记录类型使用大括号:
record Point : Set where
constructor mkPoint
field
x : Nat
y : Nat
记录值使用大括号:
point1 : Point
point1 = { x = 0; y = 0 }
函数应用使用小括号:
add : Nat -> Nat -> Nat
add x y = x + y
result : Nat
result = add 3 5
列表类型使用方括号:
list : List Nat
list = [1, 2, 3]
列表值使用方括号:
head : List Nat -> Nat
head [] = 0
head (x :: xs) = x