문법 선언
문법 선언 (Syntax Declarations)
참고: 이것은 스텁(stub) 문서예요.
이제 식별자를 바인딩하는 사용자 정의 문법을 선언할 수 있게 됐어요. 예:
record Σ (A : Set) (B : A → Set) : Set where
constructor _,_
field fst : A
snd : B fst
syntax Σ A (λ x → B) = [ x ∈ A ] × B
witness : ∀ {A B} → [ x ∈ A ] × B → A
witness (x , _) = x
Σ에 대한 문법 선언은 x가 B에서는 스코프 안에 있지만 A에서는 아님을 의미해요.
문법 선언과 함께 결합도(fixity) 선언을 줄 수 있어요:
infix 5 Σ
syntax Σ A (λ x → B) = [ x ∈ A ] × B
결합도는 이름이 아니라 문법에 적용돼요. 문법 선언은 또한 보통의, 비-연산자 이름으로 제한돼요. 다음 선언은 허용되지 않아요:
syntax _==_ x y = x === y
문법 선언은 선형(linear)이어야 해요. 다음 선언은 허용되지 않아요:
syntax wrong x = x + x
문법 선언은 암시적 인자를 가질 수 있어요. 예를 들어:
id : ∀ {a}{A : Set a} -> A -> A
id x = x
syntax id {A} x = x ∈ A
모든 밑줄을 포함한 이름으로 미적용(unapplied)으로 사용할 수 있거나, 밑줄 중 일부만 인자로 바꿔 부분 적용할 수 있는 mixfix 연산자와 달리, 문법은 완전히 적용되어야 해요.