From b1413c525c6daa4c8feccfb01c76d6748a320526 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 21 Jun 2016 09:57:21 -0700 Subject: [PATCH] chore(library/init/meta/tactic): add small comment --- library/init/meta/tactic.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index beda8d2365..201ec058ef 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -84,9 +84,11 @@ meta_constant clear : name → tactic unit /- Clear the given free-variable. The tactic fails if the given expression is not a free variable. -/ meta_constant clear_fv : expr → tactic unit meta_constant revert_lst : list name → tactic unit -meta_constant infer_type : expr → tactic expr meta_constant whnf : expr → tactic expr meta_constant unify_core : expr → expr → transparency → tactic unit +/- Infer the type of the given expression. + Remark: transparency does not affect type inference -/ +meta_constant infer_type : expr → tactic expr meta_constant get_local : name → tactic expr /- Return the hypothesis in the main goal. Fail if tactic_state does not have any goal left. -/ meta_constant local_context : tactic (list expr)