From 677e0aeef6140b4c29b7e9782a8988b8126e959b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 5 Nov 2014 11:55:41 -0800 Subject: [PATCH] fix(frontends/lean/structure_cmd): accept ': Type' when universe levels are not specified --- src/frontends/lean/structure_cmd.cpp | 17 ++++++++++++----- tests/lean/run/record9.lean | 8 ++++++++ 2 files changed, 20 insertions(+), 5 deletions(-) create mode 100644 tests/lean/run/record9.lean diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 40c7060a5..9a13cec64 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -213,11 +213,18 @@ struct structure_cmd_fn { m_type = m_p.parse_expr(); if (!is_sort(m_type)) throw parser_error("invalid 'structure', 'Type' expected", pos); - if (has_placeholder(m_type)) - throw_explicit_universe(pos); - level l = sort_level(m_type); - if (m_env.impredicative() && !is_not_zero(l)) - throw parser_error("invalid 'structure', the resultant universe level should not be zero for any universe parameter assignment", pos); + if (m_infer_result_universe) { + if (!is_placeholder(sort_level(m_type))) + throw parser_error("invalid 'structure', resultant universe level is computed " + "automatically when universe level parameters are not provided", pos); + } else { + if (has_placeholder(m_type)) + throw_explicit_universe(pos); + level l = sort_level(m_type); + if (m_env.impredicative() && !is_not_zero(l)) + throw parser_error("invalid 'structure', the resultant universe level should not be zero " + "for any universe parameter assignment", pos); + } } else { if (!m_infer_result_universe) throw_explicit_universe(pos); diff --git a/tests/lean/run/record9.lean b/tests/lean/run/record9.lean new file mode 100644 index 000000000..1fe1fa379 --- /dev/null +++ b/tests/lean/run/record9.lean @@ -0,0 +1,8 @@ +import logic + +constant fibrant : Type → Prop + +structure Fib : Type := +{type : Type} (pred : fibrant type) + +check Fib.mk