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.