From 6eeccdd67576ae32c19da2ca63189d9a39e9b6bd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 20 Feb 2021 07:52:42 -0800 Subject: [PATCH] test: for field auto implicit bound feature --- tests/lean/run/fieldAutoBound.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 tests/lean/run/fieldAutoBound.lean diff --git a/tests/lean/run/fieldAutoBound.lean b/tests/lean/run/fieldAutoBound.lean new file mode 100644 index 0000000000..847eab275e --- /dev/null +++ b/tests/lean/run/fieldAutoBound.lean @@ -0,0 +1,10 @@ +namespace Test + +open Function + +class LawfulFunctor (f : Type u → Type v) [Functor f] : Prop where + map_const : (Functor.mapConst : α → f β → f α) = Functor.map ∘ const β + id_map (x : f α) : id <$> x = x + comp_map (g : α → β) (h : β → γ) (x : f α) : (h ∘ g) <$> x = h <$> g <$> x + +end Test