michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(library/tactic): remove unnecessary file

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-27 07:02:13 -07:00
parent f1d8d8dcf9
commit b4e4c4d610
1 changed files with 0 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/library/tactic/assignment.h
View file

@ -1,20 +0,0 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "kernel/metavar.h"
namespace lean {
/**
\brief Wrapper for metavar_env that only allows us to access the assignment.
*/
class assignment {
metavar_env m_menv;
public:
assignment(metavar_env const & menv):m_menv(menv) {}
optional<expr> operator()(name const & mvar) const { return m_menv->get_subst(mvar); }
};
}