3 ms·
It reminds me of Idris, where the types can actually run programs (at compile time) as long as they can be proved to terminate, which is more often than I thoug
by mejutoco 4y ago
It reminds me of Idris, where the types can actually run programs (at compile time) as long as they can be proved to terminate, which is more often than I though.