함수 인자 quantifier를 생략하거나 중괄호로 감싸면 묵시적으로 적용됨.


표준 라이브러리에서 가져온 데이터 정의


data Nat = Z | S Nat


data (=) : a -> b -> Type where

Refl : a=a


= 타입은 두 값이 같은걸 표현함.

sym : x=y -> y=x

trans : x=y -> y=z -> x=z

cong : x=y -> f x = f y

이 함수들로 간단히 다룰 수 있음.


근데 이걸로 좀 부족해서

trans2 : x=y -> x=x' -> y=y' -> x'=y' 을 정의함.

이름이 적합한지는 잘 모르겠다


덧셈도 표준 라이브러리에 정의되있음

Z+n = n

(S m)+n = S (m+n)


addZl : Z가 좌항등원

addZr: Z가 우항등원


resolvel

resolver : 뭐라 부를지 모르겠는데, 그냥 S랑 +순서 바꾸는거

resolve2: 1+(1+(m+n)) = (m+1)+(n+1)


commute0 : 0,n 교환법칙

commute : 덧셈 교환법칙


associate : 덧셈 결합법칙




일단 이런 느낌인데, 구현은 설명할 자신이 없네

나도 아직 헷갈려서ㅋㅋㅋ