This is the HoTT snapshot

AndresTFG · Jan 3, 2017 · 9e38ae2 · 9e38ae2
1 parent 41c9533
commit 9e38ae2
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/01_Introduction.org b/01_Introduction.org
@@ -84,6 +84,12 @@ is more flexible in other ways, too. It comes with an Emacs mode that
 offers powerful support for writing and debugging proofs, and is much
 better suited for serious use.
 
+At this moment, the active development branch for Lean does not support
+homotopy type theory. The tutorial you are reading now is for the Lean
+snapshot which has been preserved for working in homotopy type theory.
+The tutorial for the active development branch can be found at
+[[https://leanprover.github.io/theorem_proving_in_lean/]].
+
 ** About this Book
 
 This book is designed to teach you to develop and verify proofs in