From bc7f4fd02b0378d389e6e8cb7c16d256b8207832 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 15 Apr 2022 09:55:10 -0700 Subject: [PATCH] test: `hasCSimpAttribute` --- tests/lean/run/csimpAttrFn.lean | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 tests/lean/run/csimpAttrFn.lean diff --git a/tests/lean/run/csimpAttrFn.lean b/tests/lean/run/csimpAttrFn.lean new file mode 100644 index 0000000000..382d4145ce --- /dev/null +++ b/tests/lean/run/csimpAttrFn.lean @@ -0,0 +1,8 @@ +import Lean + +open Lean +open Lean.Compiler + +#eval (do assert! hasCSimpAttribute (← getEnv) ``List.map_eq_mapTR : MetaM Unit) +#eval (do assert! hasCSimpAttribute (← getEnv) ``List.append_eq_appendTR : MetaM Unit) +#eval (do assert! !hasCSimpAttribute (← getEnv) ``List.append : MetaM Unit)