From 1063905d07c841effeb0caf184bbf6ccdacc9004 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 22 Jun 2018 12:39:16 -0700
Subject: [PATCH] chore(kernel/expr): reorder constructors and fix typo

---
 library/init/lean/expr.lean | 2 +-
 src/kernel/expr.h           | 8 ++++----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/library/init/lean/expr.lean b/library/init/lean/expr.lean
index 316927cbe0..70adb8189b 100644
--- a/library/init/lean/expr.lean
+++ b/library/init/lean/expr.lean
@@ -18,9 +18,9 @@ inductive binder_info
 inductive expr
 | bvar  : nat → expr                                -- bound variables
 | fvar  : name → expr                               -- free variables
+| mvar  : name → expr → expr                        -- (temporary) meta variables
 | sort  : level → expr                              -- Sort
 | const : name → list level → expr                  -- constants
-| mvar  : name → expr → expr                        -- (temporary) meta variables
 | app   : expr → expr → expr                        -- application
 | lam   : name → binder_info → expr → expr → expr   -- lambda abstraction
 | pi    : name → binder_info → expr → expr → expr   -- Pi
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 5fd54d2ea6..b25d5283e9 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -73,11 +73,11 @@ inline deserializer & operator>>(deserializer & d, literal & l) { l = read_liter
    Expressions
 
 inductive expr
-| bvar  : nat → expr   -- bound variables
-| fvar  : name → expr  -- free variables
+| bvar  : nat → expr          -- bound variables
+| fvar  : name → expr         -- free variables
+| mvar  : name → expr → expr
 | sort  : level → expr
 | const : name → list level → expr
-| mvar  : name → name → expr → expr
 | app   : expr → expr → expr
 | lam   : name → binder_info → expr → expr → expr
 | pi    : name → binder_info → expr → expr → expr
@@ -89,7 +89,7 @@ inductive expr
 | quote : bool → expr → expr
 
 */
-enum class expr_kind { BVar, FVar, Sort, Const, MVar, App, Lambda, Pi, Let, Lit, MData, Proj, Quote };
+enum class expr_kind { BVar, FVar, MVar, Sort, Const, App, Lambda, Pi, Let, Lit, MData, Proj, Quote };
 class expr : public object_ref {
     explicit expr(object * o):object_ref(o) { inc(o); }
     explicit expr(object_ref && o):object_ref(o) {}