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)