일단 재밌기는 함 ㅋㅋㅋㅋ
증명을 formal하게 쓰는거라.. 뭐 쓸모없는 짓일 수도 있지만 흥미로움.
난이도는 확실히 하스켈보다 어려움.. 좀 더 깊게 들어가면 대가리 깨질듯
그리고 하스켈 타입 시스템 + 커리 하워드 동형 같은걸 기본적으로 좀 배우고 시작해야됨
이런거 만드는 사람들은 뇌 구조가 어떻게 되있는건지..
일단 재밌기는 함 ㅋㅋㅋㅋ
증명을 formal하게 쓰는거라.. 뭐 쓸모없는 짓일 수도 있지만 흥미로움.
난이도는 확실히 하스켈보다 어려움.. 좀 더 깊게 들어가면 대가리 깨질듯
그리고 하스켈 타입 시스템 + 커리 하워드 동형 같은걸 기본적으로 좀 배우고 시작해야됨
이런거 만드는 사람들은 뇌 구조가 어떻게 되있는건지..
몬읽겠다 ㄷㄷ
dendent type system이라 타입 생성에 value를 쓸 수 있고, 저기서 =가 타입 생성자임. 좌우에 오는게 같은 값이면 Refl : x -> x -> x = x 생성자로 값을 만들 수 있음.
addZl 코드부터 해석글좀 써주셈
코드가 ㄹㅇ 수학 증명식마냥 돼있누
잠만 글 따로 써봄
덧셈의 교환법칙은 공리 아님?
교환법칙이 성립안하면 덧셈이라고 안부르지. 근데 페아노 공리에서 교환법칙 유도할 수 있음.