Extend with product types or records? #2
Description
In section 2.1 Dunfield and Krishnaswami explain that sum, product and recursive types can be easily added to this type checker. I'm very new to type theory and it's not very clear how to do so, an example here would be very helpful.