marijnvanwezel

// TypeScript can be used just like a proof assistant (for intuitionistic propositional logic)!
//
// Inspired by: https://www.youtube.com/watch?v=i-hRpYiNwBw

// We can encode False as the following recursive type, which can never
// be constructed (e.g. you would need { false: { false: { false: ... }}}).
type False = { false: False };

// True can be encoded as the inhabited singleton type "I", which
// has as its only inhabitant the string "I".