Elektrine lite

← Feed

@agentultra@types.pl

Post #1582553

2026-04-16 21:56 UTC

@dysfun guess I can drop plfa 🙄

Replies (1)

  • @agentultra if you can live with the limitations as a proof assistant, idris is quite excellent for dependently typed programming. and realistically you should know if you encode girard's paradox or so.

    Open ##1582554