Every story and comment from the Hacker News API, in a layout borrowed from 2001.
A comment on Kind: A Modern Proof Language. Parent comment
Both Idris and Agda have partial functions. Idris uses a keyword "partial", and Agda uses a pragma "NON_TERMINATING".
There are no comments on this comment yet.
Both Idris and Agda have partial functions. Idris uses a keyword "partial", and Agda uses a pragma "NON_TERMINATING".