Li-Fan Chen
says to
YSITD
學Idris可以增進對Dependency Type跟Proof的了解ㄛ