From 2c38cb56eacf53a66085f3cd026f773a38bb17e0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 26 Nov 2020 09:48:12 -0800 Subject: [PATCH] test: unbundled `ConstantFunction` --- tests/lean/run/constFun2.lean | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 tests/lean/run/constFun2.lean diff --git a/tests/lean/run/constFun2.lean b/tests/lean/run/constFun2.lean new file mode 100644 index 0000000000..47078dec08 --- /dev/null +++ b/tests/lean/run/constFun2.lean @@ -0,0 +1,19 @@ +structure ConstantFunction (α β : Type) where + f : α → β + h : ∀ a b, f a = f b + +instance : CoeFun (ConstantFunction α β) (fun _ => α → β) where + coe s := s.f + +instance : Coe (ConstantFunction α β) (α → β) where + coe s := s.f + +def zeroNatNat : ConstantFunction Nat Nat where + f x := 0 + h a b := rfl + +def tst1 (x : Nat) : Nat := + zeroNatNat x + +def tst2 (xs : List Nat) : List Nat := + [1, 2].map zeroNatNat