Revision #3445 → #3957 · back to history
addedAutomath21268a7fce2b
addedElementary Theory of the Category of Sets (ETCS)3eeaf8f12423
addedBateson's theory of logical typesf212b09c7e21
addedTurnstile symbol for judgmentsa1045b813473
addedGentzen-style deduction (horizontal-line notation)f553685caaf9
addedUninhabited type via a function to it from a supposed inhabitant7d44fbef0e2b
addedInhabited type via a function into iteea7c06cfb04
addedProgram synthesis from type specifications5dcb2659e8c4
addedType inference1bc7f1d3db08
addedInduction-recursion74a489adf51c