max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(*): replace "'^.' notation" with "field notation", pretty print using "."

Browse source
This commit is contained in:
Sebastian Ullrich 2017-03-30 15:53:36 +02:00 • committed by Leonardo de Moura
parent 93fdfdc4b6
commit cd013f22c0
17 changed files with 63 additions and 63 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/builtin_exprs.cpp
View file

@ -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) {

10
src/frontends/lean/elaborator.cpp
View file

@ -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<expr> const & args, optional<exp
return visit_base_app(new_proj, amask, new_args, expected_type, ref);
} else {
if (i >= 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<expr> const & args, optional<exp
}
proj_type = binding_body(proj_type);
}
throw elaborator_exception(ref, sstream() << "invalid '^.' notation, function '" << full_fname << "' does not have explicit argument with type ("
throw elaborator_exception(ref, sstream() << "invalid field notation, function '" << full_fname << "' does not have explicit argument with type ("
<< struct_name << " ...)");
} else {
expr new_fn = visit_function(fn, has_args, ref);
@ -2390,7 +2390,7 @@ name elaborator::field_to_decl(expr const & e, expr const & s, expr const & s_ty
expr I = get_app_fn(s_type);
if (!is_constant(I)) {
auto pp_fn = mk_pp_ctx();
throw elaborator_exception(e, format("invalid '^.' notation, type is not of the form (C ...) where C is a constant") +
throw elaborator_exception(e, format("invalid field notation, type is not of the form (C ...) where C is a constant") +
pp_indent(pp_fn, s) +
line() + format("has type") +
pp_indent(pp_fn, s_type));
@ -2421,7 +2421,7 @@ name elaborator::field_to_decl(expr const & e, expr const & s, expr const & s_ty
name full_fname = const_name(I) + fname;
if (!m_env.find(full_fname)) {
auto pp_fn = mk_pp_ctx();
throw elaborator_exception(e, format("invalid '^.' notation, '") + format(fname) + format("'") +
throw elaborator_exception(e, format("invalid field notation, '") + format(fname) + format("'") +
format(" is not a valid \"field\" because environment does not contain ") +
format("'") + format(full_fname) + format("'") +
pp_indent(pp_fn, s) +

6
src/frontends/lean/pp.cpp
View file

@ -818,10 +818,10 @@ static bool is_field_notation_candidate(environment const & env, expr const & e,
if (!info) return false; /* it is not a projection */
if (get_app_num_args(e) != info->m_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 {

2
src/frontends/lean/util.cpp
View file

@ -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;

2
src/library/pp_options.cpp
View file

@ -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");

6
tests/lean/1279.lean.expected.out
View file

@ -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

2
tests/lean/assertion1.lean.expected.out
View file

@ -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 ...)

2
tests/lean/coe6.lean.expected.out
View file

@ -1 +1 @@
λ (a b : ↥g), g^.mul a b : ↥g → ↥g → g^.carrier
λ (a b : ↥g), g.mul a b : ↥g → ↥g → g.carrier

4
tests/lean/field_access.lean.expected.out
View file

@ -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

8
tests/lean/interactive/complete_field.lean.expected.out
View file

@ -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}

12
tests/lean/pp_struct.lean.expected.out
View file

@ -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 : ℕ

22
tests/lean/proj_notation.lean.expected.out
View file

@ -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 → ℕ

4
tests/lean/set_of.lean.expected.out
View file

@ -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 (ℕ × ℕ)

2
tests/lean/uni_bug1.lean.expected.out
View file

@ -1 +1 @@
f 1 0 (Rtrue ((1, 0)^.fst) 0) : ℕ
f 1 0 (Rtrue ((1, 0).fst) 0) : ℕ

12
tests/lean/whnf.lean.expected.out
View file

@ -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

6
tests/lean/whnf_cache_bug.lean.expected.out
View file

@ -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)

24
tests/lean/whnf_core1.lean.expected.out
View file

@ -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