From c6726d22ec2d3006b57b77a1e1970eff141ea539 Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@gmail.com>
Date: Thu, 5 May 2016 08:49:45 -0700
Subject: [PATCH] doc(export_format): minor fixes

---
 doc/export_format.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/doc/export_format.md b/doc/export_format.md
index a0bd405ed..7b5a86000 100644
--- a/doc/export_format.md
+++ b/doc/export_format.md
@@ -199,10 +199,10 @@ Inductive definitions
 
 Inductive datatype declarations have the following form:
 ```
-#IND <name:nidx> <numParams:integer> <lpNames:nidx>* | <type:eidx> <numIntroRules:integer>
-#IR <irName:nidx> <irType:eidx>
+#IND <numParams:integer> <lpNames:nidx>* | <indName:nidx> <indType:eidx> <numIntroRules:integer>
+#INTRO <irName:nidx> <irType:eidx>
 ...
-#IR <irName:nidx> <irType:eidx>
+#INTRO <irName:nidx> <irType:eidx>
 ```
 For example, the following inductive type declaration
 ```lean