From 06f9e7bfddf5fb3ba609364ca229465b8feeaa63 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 25 Jun 2014 18:12:23 -0700 Subject: [PATCH] fix(build): add missing file Signed-off-by: Leonardo de Moura --- src/frontends/lean/elaborator.h | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 src/frontends/lean/elaborator.h diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h new file mode 100644 index 0000000000..32623456ce --- /dev/null +++ b/src/frontends/lean/elaborator.h @@ -0,0 +1,19 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include "util/list.h" +#include "kernel/environment.h" +#include "kernel/metavar.h" +#include "library/io_state.h" + +namespace lean { +expr elaborate(environment const & env, io_state const & ios, expr const & e, name_generator const & ngen, + substitution const & s = substitution(), list const & ctx = list()); +expr elaborate(environment const & env, io_state const & ios, expr const & e); +std::pair elaborate(environment const & env, io_state const & ios, name const & n, expr const & t, expr const & v); +}