Some of the features mentioned in this document only work on the beta or Dev channel. To change your channel:
- chrome://help in a browser window
- Click Detailed Build Information
- Change Channel
- Select Beta (Or Dev, if you're feeling adventurous)
| inductive foo | |
| | mk1 : nat → nat → foo | |
| | mk2 : nat → bool → foo | |
| example (a : foo) : nat := | |
| begin | |
| /- All new hypotheses are named 'a' -/ | |
| cases a | |
| end |
(by @andrestaltz)
If you prefer to watch video tutorials with live-coding, then check out this series I recorded with the same contents as in this article: Egghead.io - Introduction to Reactive Programming.