diff --git a/library/init/lean/expr.lean b/library/init/lean/expr.lean
new file mode 100644
index 0000000000..78576eabac
--- /dev/null
+++ b/library/init/lean/expr.lean
@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2018 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.lean.level
+
+namespace lean
+
+inductive literal
+| str_val (val : string)
+| nat_val (val : nat)
+
+inductive binder_info
+| default | implicit | strict_implicit | inst_implicit | aux_decl
+
+inductive expr
+| lit   : literal → expr                             -- literals
+| bvar  : nat → expr                                 -- bound variables
+| fvar  : name → expr                                -- free variables
+| mvar  : name → expr → expr                         -- (temporary) meta variables
+| const : name → list level → expr                   -- constants
+| sort  : level → expr                               -- Sort
+| app   : expr → expr → expr                         -- application
+| proj  : nat → expr → expr                          -- projection
+| lam   : name → binder_info → expr → expr → expr    -- lambda abstraction
+| pi    : name → binder_info → expr → expr → expr    -- Pi
+| elet  : name → expr → expr → expr → expr           -- let expressions
+| mdata : name → list (name × literal) → expr → expr -- metadata
+-- TODO: quote constructor will be deleted.
+| quote : bool → expr → expr
+
+end lean