From cd013f22c0168a8533efa6a4ddce7c7b42d70f89 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 30 Mar 2017 15:53:36 +0200 Subject: [PATCH] chore(*): replace "'^.' notation" with "field notation", pretty print using "." --- src/frontends/lean/builtin_exprs.cpp | 2 +- src/frontends/lean/elaborator.cpp | 10 ++++---- src/frontends/lean/pp.cpp | 6 ++--- src/frontends/lean/util.cpp | 2 +- src/library/pp_options.cpp | 2 +- tests/lean/1279.lean.expected.out | 6 ++--- tests/lean/assertion1.lean.expected.out | 2 +- tests/lean/coe6.lean.expected.out | 2 +- tests/lean/field_access.lean.expected.out | 4 ++-- .../complete_field.lean.expected.out | 8 +++---- tests/lean/pp_struct.lean.expected.out | 12 +++++----- tests/lean/proj_notation.lean.expected.out | 22 ++++++++--------- tests/lean/set_of.lean.expected.out | 4 ++-- tests/lean/uni_bug1.lean.expected.out | 2 +- tests/lean/whnf.lean.expected.out | 12 +++++----- tests/lean/whnf_cache_bug.lean.expected.out | 6 ++--- tests/lean/whnf_core1.lean.expected.out | 24 +++++++++---------- 17 files changed, 63 insertions(+), 63 deletions(-) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 768da75b10..2e5d432e6d 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -1017,7 +1017,7 @@ static expr parse_field(parser_state & p, unsigned, expr const * args, pos_info throw parser_error("invalid projection, index must be greater than 0", num_pos); return p.save_pos(mk_field_notation(args[0], fidx), pos); } else { - name field = p.check_id_next("invalid '^.' notation, identifier or numeral expected"); + name field = p.check_id_next("identifier or numeral expected"); return p.save_pos(mk_field_notation(args[0], field), pos); } } catch (break_at_pos_exception & ex) { diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index e0cf7ec549..c384e28a63 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -925,7 +925,7 @@ expr elaborator::visit_function(expr const & fn, bool has_args, expr const & ref throw elaborator_exception(ref, "placeholders '_' cannot be used where a function is expected"); } if (is_field_notation(fn)) - throw elaborator_exception(ref, "invalid occurrence of '^.' notation"); + throw elaborator_exception(ref, "invalid occurrence of field notation"); expr r; switch (fn.kind()) { case expr_kind::Var: @@ -1903,7 +1903,7 @@ expr elaborator::visit_app_core(expr fn, buffer const & args, optional= args.size()) { - throw elaborator_exception(ref, sstream() << "invalid '^.' notation, insufficient number of arguments for '" + throw elaborator_exception(ref, sstream() << "invalid field notation, insufficient number of arguments for '" << full_fname << "'"); } new_args.push_back(args[i]); @@ -1912,7 +1912,7 @@ expr elaborator::visit_app_core(expr fn, buffer const & args, optionalm_nparams + 1) return false; /* If implicit arguments is true, and the structure has parameters, we should not - pretty print using the ^. notation because we will not be able to see the parameters. */ + pretty print using field notation because we will not be able to see the parameters. */ if (implicit && info->m_nparams) return false; name const & S = const_name(f).get_prefix(); - /* We should not use ^. with type classes since the structure is implicit. */ + /* We should not use field notation with type classes since the structure is implicit. */ if (is_class(env, S)) return false; return true; } @@ -832,7 +832,7 @@ auto pretty_fn::pp_field_notation(expr const & e) -> result { expr const & f = get_app_args(e, args); bool ignore_hide = true; format s_fmt = pp_child(args.back(), max_bp(), ignore_hide).fmt(); - return result(max_bp()-1, s_fmt + format("^.") + format(const_name(f).get_string())); + return result(max_bp()-1, s_fmt + format(".") + format(const_name(f).get_string())); } auto pretty_fn::pp_app(expr const & e) -> result { diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index e88748fd79..cbd679d886 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -430,7 +430,7 @@ expr freeze_names(expr const & e) { static name * g_field_notation_name = nullptr; static std::string * g_field_notation_opcode = nullptr; -[[ noreturn ]] static void throw_pn_ex() { throw exception("unexpected occurrence of '^.' notation expression"); } +[[ noreturn ]] static void throw_pn_ex() { throw exception("unexpected occurrence of field notation expression"); } class field_notation_macro_cell : public macro_definition_cell { name m_field; diff --git a/src/library/pp_options.cpp b/src/library/pp_options.cpp index 25f75e5fdc..c5134c6548 100644 --- a/src/library/pp_options.cpp +++ b/src/library/pp_options.cpp @@ -221,7 +221,7 @@ void initialize_pp_options() { "when displaying structure instances using the '{ struct_name . field_name := field_value, ... }' notation, " "this option is ignored when pp.structure_instances is false"); register_bool_option(*g_pp_structure_projections, LEAN_DEFAULT_PP_STRUCTURE_PROJECTIONS, - "(pretty printer) display structure projections using the '^.' notation"); + "(pretty printer) display structure projections using field notation"); register_bool_option(*g_pp_all, LEAN_DEFAULT_PP_ALL, "(pretty printer) display coercions, implicit parameters, proof terms, fully qualified names, universes, " "and disable beta reduction and notation during pretty printing"); diff --git a/tests/lean/1279.lean.expected.out b/tests/lean/1279.lean.expected.out index bb46a779e3..96706aa67a 100644 --- a/tests/lean/1279.lean.expected.out +++ b/tests/lean/1279.lean.expected.out @@ -1,8 +1,8 @@ 1279.lean:12:33: error: type mismatch at application - source^.compose g f + source.compose g f term f has type - source^.Hom A B + source.Hom A B but is expected to have type - source^.Hom C ?m_1 + source.Hom C ?m_1 diff --git a/tests/lean/assertion1.lean.expected.out b/tests/lean/assertion1.lean.expected.out index 169a8b1b82..2f31b707b2 100644 --- a/tests/lean/assertion1.lean.expected.out +++ b/tests/lean/assertion1.lean.expected.out @@ -1 +1 @@ -assertion1.lean:37:21: error: invalid '^.' notation, function 'MonoidalCategory.tensorObjects' does not have explicit argument with type (MonoidalCategory ...) +assertion1.lean:37:21: error: invalid field notation, function 'MonoidalCategory.tensorObjects' does not have explicit argument with type (MonoidalCategory ...) diff --git a/tests/lean/coe6.lean.expected.out b/tests/lean/coe6.lean.expected.out index 8c639d531f..5b070023d5 100644 --- a/tests/lean/coe6.lean.expected.out +++ b/tests/lean/coe6.lean.expected.out @@ -1 +1 @@ -λ (a b : ↥g), g^.mul a b : ↥g → ↥g → g^.carrier +λ (a b : ↥g), g.mul a b : ↥g → ↥g → g.carrier diff --git a/tests/lean/field_access.lean.expected.out b/tests/lean/field_access.lean.expected.out index d991dee6bf..9320ce4078 100644 --- a/tests/lean/field_access.lean.expected.out +++ b/tests/lean/field_access.lean.expected.out @@ -7,11 +7,11 @@ field_access.lean:7:13: error: invalid projection, structure has only 2 field(s) (1, 2) which has type ?m_1 × ?m_2 -field_access.lean:10:1: error: invalid '^.' notation, 'forr' is not a valid "field" because environment does not contain 'list.forr' +field_access.lean:10:1: error: invalid field notation, 'forr' is not a valid "field" because environment does not contain 'list.forr' l which has type list ℕ -field_access.lean:13:1: error: invalid '^.' notation, type is not of the form (C ...) where C is a constant +field_access.lean:13:1: error: invalid field notation, type is not of the form (C ...) where C is a constant a has type A diff --git a/tests/lean/interactive/complete_field.lean.expected.out b/tests/lean/interactive/complete_field.lean.expected.out index 1ee8c474d1..114bea4699 100644 --- a/tests/lean/interactive/complete_field.lean.expected.out +++ b/tests/lean/interactive/complete_field.lean.expected.out @@ -1,7 +1,7 @@ -{"msgs":[{"caption":"","file_name":"f","pos_col":14,"pos_line":4,"severity":"error","text":"invalid '^.' notation, 'l' is not a valid \"field\" because environment does not contain 'and.l'\n h y\nwhich has type\n p y ∧ q y"}],"response":"all_messages"} -{"msgs":[{"caption":"","file_name":"f","pos_col":14,"pos_line":4,"severity":"error","text":"invalid '^.' notation, 'l' is not a valid \"field\" because environment does not contain 'and.l'\n h y\nwhich has type\n p y ∧ q y"},{"caption":"","file_name":"f","pos_col":14,"pos_line":8,"severity":"error","text":"invalid '^.' notation, 'le' is not a valid \"field\" because environment does not contain 'and.le'\n h y\nwhich has type\n p y ∧ q y"}],"response":"all_messages"} -{"msgs":[{"caption":"","file_name":"f","pos_col":14,"pos_line":4,"severity":"error","text":"invalid '^.' notation, 'l' is not a valid \"field\" because environment does not contain 'and.l'\n h y\nwhich has type\n p y ∧ q y"},{"caption":"","file_name":"f","pos_col":14,"pos_line":8,"severity":"error","text":"invalid '^.' notation, 'le' is not a valid \"field\" because environment does not contain 'and.le'\n h y\nwhich has type\n p y ∧ q y"},{"caption":"","file_name":"f","pos_col":14,"pos_line":12,"severity":"error","text":"invalid '^.' notation, 'r' is not a valid \"field\" because environment does not contain 'and.r'\n h y\nwhich has type\n p y ∧ q y"}],"response":"all_messages"} -{"msgs":[{"caption":"","file_name":"f","pos_col":14,"pos_line":4,"severity":"error","text":"invalid '^.' notation, 'l' is not a valid \"field\" because environment does not contain 'and.l'\n h y\nwhich has type\n p y ∧ q y"},{"caption":"","file_name":"f","pos_col":14,"pos_line":8,"severity":"error","text":"invalid '^.' notation, 'le' is not a valid \"field\" because environment does not contain 'and.le'\n h y\nwhich has type\n p y ∧ q y"},{"caption":"","file_name":"f","pos_col":14,"pos_line":12,"severity":"error","text":"invalid '^.' notation, 'r' is not a valid \"field\" because environment does not contain 'and.r'\n h y\nwhich has type\n p y ∧ q y"},{"caption":"","file_name":"f","pos_col":39,"pos_line":17,"severity":"error","text":"invalid '^.' notation, identifier or numeral expected"}],"response":"all_messages"} +{"msgs":[{"caption":"","file_name":"f","pos_col":14,"pos_line":4,"severity":"error","text":"invalid field notation, 'l' is not a valid \"field\" because environment does not contain 'and.l'\n h y\nwhich has type\n p y ∧ q y"}],"response":"all_messages"} +{"msgs":[{"caption":"","file_name":"f","pos_col":14,"pos_line":4,"severity":"error","text":"invalid field notation, 'l' is not a valid \"field\" because environment does not contain 'and.l'\n h y\nwhich has type\n p y ∧ q y"},{"caption":"","file_name":"f","pos_col":14,"pos_line":8,"severity":"error","text":"invalid field notation, 'le' is not a valid \"field\" because environment does not contain 'and.le'\n h y\nwhich has type\n p y ∧ q y"}],"response":"all_messages"} +{"msgs":[{"caption":"","file_name":"f","pos_col":14,"pos_line":4,"severity":"error","text":"invalid field notation, 'l' is not a valid \"field\" because environment does not contain 'and.l'\n h y\nwhich has type\n p y ∧ q y"},{"caption":"","file_name":"f","pos_col":14,"pos_line":8,"severity":"error","text":"invalid field notation, 'le' is not a valid \"field\" because environment does not contain 'and.le'\n h y\nwhich has type\n p y ∧ q y"},{"caption":"","file_name":"f","pos_col":14,"pos_line":12,"severity":"error","text":"invalid field notation, 'r' is not a valid \"field\" because environment does not contain 'and.r'\n h y\nwhich has type\n p y ∧ q y"}],"response":"all_messages"} +{"msgs":[{"caption":"","file_name":"f","pos_col":14,"pos_line":4,"severity":"error","text":"invalid field notation, 'l' is not a valid \"field\" because environment does not contain 'and.l'\n h y\nwhich has type\n p y ∧ q y"},{"caption":"","file_name":"f","pos_col":14,"pos_line":8,"severity":"error","text":"invalid field notation, 'le' is not a valid \"field\" because environment does not contain 'and.le'\n h y\nwhich has type\n p y ∧ q y"},{"caption":"","file_name":"f","pos_col":14,"pos_line":12,"severity":"error","text":"invalid field notation, 'r' is not a valid \"field\" because environment does not contain 'and.r'\n h y\nwhich has type\n p y ∧ q y"},{"caption":"","file_name":"f","pos_col":39,"pos_line":17,"severity":"error","text":"identifier or numeral expected"}],"response":"all_messages"} {"message":"file invalidated","response":"ok","seq_num":0} {"completions":[{"source":,"text":"left","type":"?a ∧ ?b → ?a"},{"source":{"column":14,"file":"/library/init/logic.lean","line":405},"text":"left_comm","type":"?a ∧ ?b ∧ ?c ↔ ?b ∧ ?a ∧ ?c"}],"prefix":"l","response":"ok","seq_num":5} {"completions":[{"source":,"text":"left","type":"?a ∧ ?b → ?a"},{"source":{"column":14,"file":"/library/init/logic.lean","line":405},"text":"left_comm","type":"?a ∧ ?b ∧ ?c ↔ ?b ∧ ?a ∧ ?c"}],"prefix":"le","response":"ok","seq_num":9} diff --git a/tests/lean/pp_struct.lean.expected.out b/tests/lean/pp_struct.lean.expected.out index 07d4826f53..beb16fd88d 100644 --- a/tests/lean/pp_struct.lean.expected.out +++ b/tests/lean/pp_struct.lean.expected.out @@ -6,7 +6,7 @@ let s : foo := in v1 + v2 + v3 + v4, y := 20, z := tt} -in s^.x + s^.y : +in s.x + s.y : ℕ let s : foo := {foo . @@ -17,12 +17,12 @@ let s : foo := in v1 + v2 + v3 + v4, y := 20, z := tt} -in s^.x + s^.y : +in s.x + s.y : ℕ foo.mk 10 20 ff : foo {foo . x := 10, y := 20, z := ff} : foo {x := 10, y := 20, z := ff} : foo -{x := 10, y := 20, z := ff}^.x : ℕ -(1, 2)^.fst : ℕ -(boo 1 1)^.fst : ℕ -(h 0)^.fn 10 20 : ℕ +{x := 10, y := 20, z := ff}.x : ℕ +(1, 2).fst : ℕ +(boo 1 1).fst : ℕ +(h 0).fn 10 20 : ℕ diff --git a/tests/lean/proj_notation.lean.expected.out b/tests/lean/proj_notation.lean.expected.out index 6f2dbafe33..8f1bd91311 100644 --- a/tests/lean/proj_notation.lean.expected.out +++ b/tests/lean/proj_notation.lean.expected.out @@ -1,11 +1,11 @@ -p^.fst : ℕ -p^.fst : ℕ -p^.snd : ℕ -p^.snd : ℕ -f (p^.fst) : ℕ -p^.fst + p^.snd : ℕ -λ (c : car), (c^.pos)^.x : car → ℕ -proj_notation.lean:29:19: error: invalid '^.' notation, 'fst' is not a valid "field" because environment does not contain 'car.fst' +p.fst : ℕ +p.fst : ℕ +p.snd : ℕ +p.snd : ℕ +f (p.fst) : ℕ +p.fst + p.snd : ℕ +λ (c : car), (c.pos).x : car → ℕ +proj_notation.lean:29:19: error: invalid field notation, 'fst' is not a valid "field" because environment does not contain 'car.fst' c which has type car @@ -18,6 +18,6 @@ proj_notation.lean:35:19: error: invalid projection, structure expected n has type ℕ -p^.fst : ℕ -p^.snd : ℕ -λ (c : car), (c^.pos)^.y : car → ℕ +p.fst : ℕ +p.snd : ℕ +λ (c : car), (c.pos).y : car → ℕ diff --git a/tests/lean/set_of.lean.expected.out b/tests/lean/set_of.lean.expected.out index 675b7538ca..f2ed5cb2d6 100644 --- a/tests/lean/set_of.lean.expected.out +++ b/tests/lean/set_of.lean.expected.out @@ -1,6 +1,6 @@ {x : ℕ | x > 0} : set ℕ {x : ℕ | x > 0} : set ℕ -{p : ℕ × ℕ | p^.fst > p^.snd} : set (ℕ × ℕ) +{p : ℕ × ℕ | p.fst > p.snd} : set (ℕ × ℕ) {x | x > 0} : set ℕ {x | x > 0} : set ℕ -{p | p^.fst > p^.snd} : set (ℕ × ℕ) +{p | p.fst > p.snd} : set (ℕ × ℕ) diff --git a/tests/lean/uni_bug1.lean.expected.out b/tests/lean/uni_bug1.lean.expected.out index 165b8b7e27..064adc9284 100644 --- a/tests/lean/uni_bug1.lean.expected.out +++ b/tests/lean/uni_bug1.lean.expected.out @@ -1 +1 @@ -f 1 0 (Rtrue ((1, 0)^.fst) 0) : ℕ +f 1 0 (Rtrue ((1, 0).fst) 0) : ℕ diff --git a/tests/lean/whnf.lean.expected.out b/tests/lean/whnf.lean.expected.out index 2250065628..42c057e145 100644 --- a/tests/lean/whnf.lean.expected.out +++ b/tests/lean/whnf.lean.expected.out @@ -3,7 +3,7 @@ succ ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ ((_F^.fst)^.fst a)) + (λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ ((_F.fst).fst a)) _F) a_1 a @@ -15,7 +15,7 @@ succ ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ ((_F^.fst)^.fst a)) + (λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ ((_F.fst).fst a)) _F) a_1 a @@ -24,7 +24,7 @@ succ ⟨ih_1, punit.star⟩, ⟨ih_1, punit.star⟩⟩) 0, - punit.star⟩^.fst)^.fst + punit.star⟩.fst).fst 2) 3 succ @@ -32,7 +32,7 @@ succ ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ ((_F^.fst)^.fst a)) + (λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ ((_F.fst).fst a)) _F) a_1 a @@ -44,7 +44,7 @@ succ ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ ((_F^.fst)^.fst a)) + (λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ ((_F.fst).fst a)) _F) a_1 a @@ -53,6 +53,6 @@ succ ⟨ih_1, punit.star⟩, ⟨ih_1, punit.star⟩⟩) 0, - punit.star⟩^.fst)^.fst + punit.star⟩.fst).fst a) succ a diff --git a/tests/lean/whnf_cache_bug.lean.expected.out b/tests/lean/whnf_cache_bug.lean.expected.out index 3476f290bf..a2d1ec1a5d 100644 --- a/tests/lean/whnf_cache_bug.lean.expected.out +++ b/tests/lean/whnf_cache_bug.lean.expected.out @@ -4,7 +4,7 @@ nat.succ ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F.fst).fst a)) _F) a_1 a @@ -16,7 +16,7 @@ nat.succ ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F.fst).fst a)) _F) a_1 a @@ -25,5 +25,5 @@ nat.succ ⟨ih_1, punit.star⟩, ⟨ih_1, punit.star⟩⟩) 0, - punit.star⟩^.fst)^.fst + punit.star⟩.fst).fst 1) diff --git a/tests/lean/whnf_core1.lean.expected.out b/tests/lean/whnf_core1.lean.expected.out index 0b1e48c7bb..8858339d87 100644 --- a/tests/lean/whnf_core1.lean.expected.out +++ b/tests/lean/whnf_core1.lean.expected.out @@ -3,7 +3,7 @@ nat.succ ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F.fst).fst a)) _F) a_1 a @@ -15,7 +15,7 @@ nat.succ ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F.fst).fst a)) _F) a_1 a @@ -27,7 +27,7 @@ nat.succ ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F.fst).fst a)) _F) a_1 a @@ -39,7 +39,7 @@ nat.succ ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F.fst).fst a)) _F) a_1 a @@ -48,16 +48,16 @@ nat.succ ⟨ih_1, punit.star⟩, ⟨ih_1, punit.star⟩⟩) 0, - punit.star⟩^.fst)^.fst + punit.star⟩.fst).fst 1), - punit.star⟩^.fst)^.fst + punit.star⟩.fst).fst a) nat.succ ((⟨nat.rec ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F.fst).fst a)) _F) a_1 a @@ -69,7 +69,7 @@ nat.succ ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F.fst).fst a)) _F) a_1 a @@ -81,7 +81,7 @@ nat.succ ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F.fst).fst a)) _F) a_1 a @@ -93,7 +93,7 @@ nat.succ ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F.fst).fst a)) _F) a_1 a @@ -102,9 +102,9 @@ nat.succ ⟨ih_1, punit.star⟩, ⟨ih_1, punit.star⟩⟩) 0, - punit.star⟩^.fst)^.fst + punit.star⟩.fst).fst 1), - punit.star⟩^.fst)^.fst + punit.star⟩.fst).fst a) f a a + 2