From abb63cbfa66cb51e4d157cbd91a647baf2bc76ad Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 Jan 2017 09:01:20 -0800 Subject: [PATCH] fix(frontends/lean/elaborator): cactch app_exception when trying to create coercion closes #1279 --- src/frontends/lean/elaborator.cpp | 2 ++ tests/lean/1279.lean | 12 ++++++++++++ tests/lean/1279.lean.expected.out | 8 ++++++++ 3 files changed, 22 insertions(+) create mode 100644 tests/lean/1279.lean create mode 100644 tests/lean/1279.lean.expected.out diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 478d390315..c0bf39e255 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -463,6 +463,8 @@ bool elaborator::is_monad(expr const & e) { try { expr m = mk_app(m_ctx, get_monad_name(), e); return static_cast(m_ctx.mk_class_instance(m)); + } catch (app_builder_exception &) { + return false; } catch (class_exception &) { return false; } diff --git a/tests/lean/1279.lean b/tests/lean/1279.lean new file mode 100644 index 0000000000..fe3930e4f5 --- /dev/null +++ b/tests/lean/1279.lean @@ -0,0 +1,12 @@ +structure Category : Type 2 := + (Obj : Type) + (Hom : Obj → Obj → Type) + (compose : Π ⦃A B C : Obj⦄, Hom A B → Hom B C → Hom A C) + +open Category + +structure Functor (source target : Category) : Type := + (onObjects : Obj source → Obj target) + (onMorphisms : Π ⦃A B : Obj source⦄, Hom source A B → Hom target (onObjects A) (onObjects B)) + (functoriality : Π ⦃A B C : Obj source⦄ (f : Hom source A B) (g : Hom source B C), + onMorphisms (compose source g f) = compose target (onMorphisms g) (onMorphisms f)) diff --git a/tests/lean/1279.lean.expected.out b/tests/lean/1279.lean.expected.out new file mode 100644 index 0000000000..7a8f0bf0aa --- /dev/null +++ b/tests/lean/1279.lean.expected.out @@ -0,0 +1,8 @@ +1279.lean:12:33: error: type mismatch at application + compose source g f +term + f +has type + Hom source A B +but is expected to have type + Hom source C ?m_1