From ce589a885ccdea477e98e4ce38d6d3a4ae8940a9 Mon Sep 17 00:00:00 2001 From: Joe Corneli Date: Fri, 29 Mar 2019 12:08:02 +0000 Subject: [PATCH] add new pow_to_pexpr rule --- src/mathematica.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/mathematica.lean b/src/mathematica.lean index fa43728..9dd18bb 100644 --- a/src/mathematica.lean +++ b/src/mathematica.lean @@ -483,6 +483,11 @@ meta def mul_to_pexpr : app_trans_pexpr_keyed_rule := ⟨"Times", λ env args, do args' ← monad.mapm (pexpr_of_mmexpr env) args, return $ pexpr_fold_op ```(1) ```(has_mul.mul) args'⟩ +@[app_to_pexpr_keyed] +meta def pow_to_pexpr : app_trans_pexpr_keyed_rule := +⟨"Power", +λ env args, do args' ← monad.mapm (pexpr_of_mmexpr env) args, return $ pexpr_fold_op ```(1) ```(has_pow.pow) args'⟩ + @[app_to_pexpr_keyed] meta def list_to_pexpr : app_trans_pexpr_keyed_rule := ⟨"List", λ env args,