[%] 어 안되네 ... ㅈㅅ

[기괴공학도(mecheng98)]

이렇게 하고 돌렸는데 안 됨

[다믜(damhiya)]

잘 하면 방법 있지 않을까

[다믜(damhiya)]

저기 pi 설마 dependent pi type에 그 pi임?

[다믜(damhiya)]

ㅈㄴ 근본 넘치네 ㅋㅋㅋㅋㅋㅋㅋㅋㅋ

[기괴공학도(mecheng98)]

forall - dc App

[다믜(damhiya)]

ㅇㅇ 그게 dependent pi type 이랑 같은거

[기괴공학도(mecheng98)]

(A → o) → o의 타입임 - dc App

[기괴공학도(mecheng98)]

o는 명제를 나타내는 타입 - dc App

[다믜(damhiya)]

type zero nat. 이라고 하면 zero의 type이 nat인 거임? 아니면 nat에 속하는 zero라는 타입을 정의한 거임?

[기괴공학도(mecheng98)]

전자 - dc App