From 9bbef4cf94c283c4d6b8d487c154019afe8c799c Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Thu, 16 Jul 2020 17:05:39 -0400 Subject: [PATCH 1/3] feat(meta/environment): the equations that lead to a given definition are now accessible in Lean code --- library/init/meta/environment.lean | 6 +- library/init/meta/tactic.lean | 7 ++ src/frontends/lean/CMakeLists.txt | 4 +- src/frontends/lean/definition_cmds.cpp | 11 ++- src/frontends/lean/eqn_api.cpp | 105 +++++++++++++++++++++++++ src/frontends/lean/eqn_api.h | 17 ++++ src/frontends/lean/init_module.cpp | 3 + tests/lean/eqn_api.lean | 29 +++++++ tests/lean/eqn_api.lean.expected.out | 12 +++ tests/lean/eqn_api2.lean | 12 +++ tests/lean/eqn_api2.lean.expected.out | 0 11 files changed, 201 insertions(+), 5 deletions(-) create mode 100644 src/frontends/lean/eqn_api.cpp create mode 100644 src/frontends/lean/eqn_api.h create mode 100644 tests/lean/eqn_api.lean create mode 100644 tests/lean/eqn_api.lean.expected.out create mode 100644 tests/lean/eqn_api2.lean create mode 100644 tests/lean/eqn_api2.lean.expected.out diff --git a/library/init/meta/environment.lean b/library/init/meta/environment.lean index 302631e291..43ee7a4597 100644 --- a/library/init/meta/environment.lean +++ b/library/init/meta/environment.lean @@ -5,7 +5,7 @@ Authors: Leonardo de Moura -/ prelude import init.meta.declaration init.meta.exceptional init.data.option.basic -import init.meta.rb_map +import init.meta.rb_map init.meta.pexpr /-- An __environment__ contains all of the declarations and notation that have been defined so far. -/ meta constant environment : Type @@ -143,6 +143,10 @@ But there are no `is_inductive`s which are not `is_ginductive`. meta constant is_ginductive : environment → name → bool /-- See the docstring for `projection_info`. -/ meta constant is_projection : environment → name → option projection_info + +/-- Get the equations specifying a certain definition -/ +meta constant defn_spec : environment → name → option pexpr + /-- Fold over declarations in the environment. -/ meta constant fold {α :Type} : environment → α → (declaration → α → α) → α /-- `relation_info env n` returns some value if n is marked as a relation in the given environment. diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 190d2e24e2..ae9e808e17 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -1552,6 +1552,13 @@ meta def is_protected_decl (n : name) : tactic bool := do env ← get_env, return $ env.is_protected n +/-- get the set of equations that specify a given +definition -/ +meta def get_defn_spec (n : name) : tactic pexpr := +do env ← get_env, + env.defn_spec n + + /-- `add_defn_equations` adds a definition specified by a list of equations. The arguments: diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index a16733f23a..df7e53060d 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -10,7 +10,7 @@ match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp brackets.cpp tactic_notation.cpp info_manager.cpp json.cpp module_parser.cpp interactive.cpp completion.cpp user_notation.cpp user_command.cpp -widget.cpp) +widget.cpp eqn_api.cpp) if(EMSCRIPTEN) add_dependencies(lean_frontend gmp) -endif() \ No newline at end of file +endif() diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index 4a7d28f3f1..cbc90455a0 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -36,6 +36,7 @@ Author: Leonardo de Moura #include "library/compiler/rec_fn_macro.h" #include "library/tactic/eqn_lemmas.h" #include "frontends/lean/parser.h" +#include "frontends/lean/eqn_api.h" #include "frontends/lean/tokens.h" #include "frontends/lean/elaborator.h" #include "frontends/lean/util.h" @@ -475,7 +476,10 @@ static environment mutual_definition_cmd_core(parser & p, decl_cmd_kind kind, cm return p.env(); bool recover_from_errors = true; - elaborator elab(env, p.get_options(), get_namespace(env) + mlocal_pp_name(fns[0]), metavar_context(), local_context(), recover_from_errors); + name full_name = get_namespace(env) + mlocal_pp_name(fns[0]); + env = store_eqn_spec(env, full_name, val); + p.set_env(env); + elaborator elab(env, p.get_options(), full_name, metavar_context(), local_context(), recover_from_errors); buffer new_params; elaborate_params(elab, params, new_params); val = replace_locals_preserving_pos_info(val, params, new_params); @@ -794,7 +798,10 @@ environment single_definition_cmd_core(parser_info & p, decl_cmd_kind kind, cmd_ return p.env(); bool recover_from_errors = p.m_error_recovery; - elaborator elab(env, p.get_options(), get_namespace(env) + mlocal_pp_name(fn), metavar_context(), local_context(), recover_from_errors); + name full_name = get_namespace(env) + mlocal_pp_name(fn); + env = store_eqn_spec(env, full_name, val); + p.set_env(env); + elaborator elab(env, p.get_options(), full_name, metavar_context(), local_context(), recover_from_errors); buffer new_params; elaborate_params(elab, params, new_params); elab.freeze_local_instances(); diff --git a/src/frontends/lean/eqn_api.cpp b/src/frontends/lean/eqn_api.cpp new file mode 100644 index 0000000000..5df7c6b8e8 --- /dev/null +++ b/src/frontends/lean/eqn_api.cpp @@ -0,0 +1,105 @@ +/* +Copyright (c) 2020 Simon Hudon. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Simon Hudon +*/ + +#include +#include "kernel/environment.h" +#include "library/module.h" +#include "library/vm/vm.h" +#include "library/vm/vm_name.h" +#include "library/vm/vm_environment.h" +#include "library/vm/vm_expr.h" +#include "library/vm/vm_option.h" +#include "library/kernel_serializer.h" + +namespace lean { + +struct eqn_info : public environment_extension { + std::map m_eqn_info; + + eqn_info() { } +}; + +struct eqn_info_reg { + unsigned m_ext_id; + eqn_info_reg() { + m_ext_id = environment::register_extension(std::make_shared(eqn_info())); + } +}; + +static eqn_info_reg * g_ext = nullptr; + +static eqn_info const & get_extension(environment const & env) { + return static_cast(env.get_extension(g_ext->m_ext_id)); +} + +static environment update(environment const & env, eqn_info const & ext) { + return env.update(g_ext->m_ext_id, std::make_shared(ext)); +} + + +struct eqn_info_modification : public modification { + LEAN_MODIFICATION("EQN_INFO") + + name m_fn; + expr m_eqns; + + eqn_info_modification(name const & fn, expr const & eqns): m_fn(fn), m_eqns(eqns) {} + + void perform(environment & env) const override { + auto ext = get_extension(env); + ext.m_eqn_info.insert(mk_pair(m_fn, m_eqns)); + env = update(env, ext); + } + + void serialize(serializer & s) const override { + s << m_fn << m_eqns; + } + + static std::shared_ptr deserialize(deserializer & d) { + name fn; expr eqns; + d >> fn >> eqns; + return std::make_shared(fn, eqns); + } +}; + +optional get_eqn_spec(environment const & env, name const & n) { + auto ext = get_extension(env); + std::map::iterator eqn = ext.m_eqn_info.find(n); + if (eqn != ext.m_eqn_info.end()) { + return optional(eqn->second); + } else { + return optional(); + } +} + +vm_obj environment_get_eqn_spec(vm_obj const & env, vm_obj const & n) { + environment env_ = to_env(env); + name n_ = to_name(n); + if (auto r = get_eqn_spec(env_, n_)) { + return mk_vm_some(to_obj(*r)); + } else { + return mk_vm_none(); + } +} + +environment store_eqn_spec(environment const & env, name const & n, expr const & e) { + return module::add_and_perform(env, std::make_shared(n, e)); +} + +void initialize_eqn_api() { + g_ext = new eqn_info_reg(); + eqn_info_modification::init(); + DECLARE_VM_BUILTIN(name({"environment", "defn_spec"}), environment_get_eqn_spec); +} + +void finalize_eqn_api() { + eqn_info_modification::finalize(); + delete g_ext; +} + + +} diff --git a/src/frontends/lean/eqn_api.h b/src/frontends/lean/eqn_api.h new file mode 100644 index 0000000000..ea12ce1adb --- /dev/null +++ b/src/frontends/lean/eqn_api.h @@ -0,0 +1,17 @@ +/* +Copyright (c) 2020 Simon Hudon. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Simon Hudon +*/ +#pragma once +#include "kernel/environment.h" + +namespace lean { + +void initialize_eqn_api(); +void finalize_eqn_api(); +environment store_eqn_spec(environment const & env, name const & n, expr const & e); +optional get_eqn_spec(environment const & env, name const & n); + +} diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp index c8a309a71b..cc04cdb918 100644 --- a/src/frontends/lean/init_module.cpp +++ b/src/frontends/lean/init_module.cpp @@ -31,6 +31,7 @@ Author: Leonardo de Moura #include "frontends/lean/user_notation.h" #include "frontends/lean/user_command.h" #include "frontends/lean/widget.h" +#include "frontends/lean/eqn_api.h" namespace lean { void initialize_frontend_lean_module() { @@ -61,8 +62,10 @@ void initialize_frontend_lean_module() { initialize_user_notation(); initialize_user_command(); initialize_widget(); + initialize_eqn_api(); } void finalize_frontend_lean_module() { + finalize_eqn_api(); finalize_user_command(); finalize_user_notation(); finalize_completion(); diff --git a/tests/lean/eqn_api.lean b/tests/lean/eqn_api.lean new file mode 100644 index 0000000000..da396133b4 --- /dev/null +++ b/tests/lean/eqn_api.lean @@ -0,0 +1,29 @@ + +import .eqn_api2 + +def foo_bar (a : Type) (x : a) : option a -> a +| none := x +| (some y) := y + +def all : bool -> bool -> bool -> bool -> bool +| ff _ _ _ := ff +| _ ff _ _ := ff +| _ _ ff _ := ff +| _ _ _ ff := ff +| _ _ _ _ := tt + +open tactic + +run_cmd do + e ← get_env, + trace "foo", + environment.defn_spec e ``foo >>= trace, + trace "foo_bar", + environment.defn_spec e ``foo_bar >>= trace, + trace "all", + environment.defn_spec e ``all >>= trace, + trace "f", + environment.defn_spec e ``f >>= trace, + trace "g", + environment.defn_spec e ``g >>= trace, + skip diff --git a/tests/lean/eqn_api.lean.expected.out b/tests/lean/eqn_api.lean.expected.out new file mode 100644 index 0000000000..ea0942d8e7 --- /dev/null +++ b/tests/lean/eqn_api.lean.expected.out @@ -0,0 +1,12 @@ +eqn_api.lean:17:0: error: failed +state: +⊢ true +foo +equations (fun (foo : (option a) -> a), (equation ((«@» foo) option.none) x)) (fun (foo : (option a) -> a) (y : 4._.15), (equation ((«@» foo) (option.some y)) y)) +foo_bar +equations (fun (foo_bar : (option a) -> a), (equation ((«@» foo_bar) option.none) x)) (fun (foo_bar : (option a) -> a) (y : 4._.21), (equation ((«@» foo_bar) (option.some y)) y)) +all +equations (fun (all : bool -> bool -> bool -> bool -> bool) (_x : 4._.4) (_x_1 : 4._.5) (_x_2 : 4._.6), (equation ((«@» all) bool.ff _x _x_1 _x_2) bool.ff)) (fun (all : bool -> bool -> bool -> bool -> bool) (_x : 4._.11) (_x_1 : 4._.12) (_x_2 : 4._.13), (equation ((«@» all) _x bool.ff _x_1 _x_2) bool.ff)) (fun (all : bool -> bool -> bool -> bool -> bool) (_x : 4._.18) (_x_1 : 4._.19) (_x_2 : 4._.20), (equation ((«@» all) _x _x_1 bool.ff _x_2) bool.ff)) (fun (all : bool -> bool -> bool -> bool -> bool) (_x : 4._.25) (_x_1 : 4._.26) (_x_2 : 4._.27), (equation ((«@» all) _x _x_1 _x_2 bool.ff) bool.ff)) (fun (all : bool -> bool -> bool -> bool -> bool) (_x : 4._.32) (_x_1 : 4._.33) (_x_2 : 4._.34) (_x_3 : 4._.35), (equation ((«@» all) _x _x_1 _x_2 _x_3) bool.tt)) +f +equations (fun (f : (list nat) -> nat) (g : (list nat) -> nat), (equation ((«@» f) list.nil) 0)) (fun (f : (list nat) -> nat) (g : (list nat) -> nat) (x : 4._.2) (xs : 4._.3), (equation ((«@» f) (list.cons x xs)) (has_add.add x (g xs)))) (fun (f : (list nat) -> nat) (g : (list nat) -> nat), (equation ((«@» g) list.nil) 0)) (fun (f : (list nat) -> nat) (g : (list nat) -> nat) (x : 4._.6) (xs : 4._.7), (equation ((«@» g) (list.cons x xs)) (f xs))) +g diff --git a/tests/lean/eqn_api2.lean b/tests/lean/eqn_api2.lean new file mode 100644 index 0000000000..ed4b626a02 --- /dev/null +++ b/tests/lean/eqn_api2.lean @@ -0,0 +1,12 @@ + +mutual def f, g +with f : list ℕ -> ℕ +| [] := 0 +| (x :: xs) := x + g xs +with g : list ℕ -> ℕ +| [] := 0 +| (x :: xs) := f xs + +def foo (a : Type) (x : a) : option a -> a +| none := x +| (some y) := y diff --git a/tests/lean/eqn_api2.lean.expected.out b/tests/lean/eqn_api2.lean.expected.out new file mode 100644 index 0000000000..e69de29bb2 From eda0f81de4e3aef6a9ecb8b3386c8d23d2763c05 Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Thu, 16 Jul 2020 19:11:31 -0400 Subject: [PATCH 2/3] fix test and make replace / fold polymorphic --- library/init/meta/expr.lean | 4 ++-- src/library/vm/vm_expr.cpp | 4 ++-- tests/lean/eqn_api.lean | 17 ++++++++++++----- tests/lean/eqn_api.lean.expected.out | 8 ++++---- 4 files changed, 20 insertions(+), 13 deletions(-) diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean index 6a82175016..844d0d16fb 100644 --- a/library/init/meta/expr.lean +++ b/library/init/meta/expr.lean @@ -158,14 +158,14 @@ meta constant expr.lt : expr → expr → bool meta constant expr.lex_lt : expr → expr → bool /-- `expr.fold e a f`: Traverses each subexpression of `e`. The `nat` passed to the folder `f` is the binder depth. -/ -meta constant expr.fold {α : Type} : expr → α → (expr → nat → α → α) → α +meta constant expr.fold {elab : opt_param bool tt} {α : Type} : expr elab → α → (expr elab → nat → α → α) → α /-- `expr.replace e f` Traverse over an expr `e` with a function `f` which can decide to replace subexpressions or not. For each subexpression `s` in the expression tree, `f s n` is called where `n` is how many binders are present above the given subexpression `s`. If `f s n` returns `none`, the children of `s` will be traversed. Otherwise if `some s'` is returned, `s'` will replace `s` and this subexpression will not be traversed further. -/ -meta constant expr.replace : expr → (expr → nat → option expr) → expr +meta constant expr.replace {elab : opt_param bool tt} : expr elab → (expr elab → nat → option (expr elab)) → expr elab /-- `abstract_local e n` replaces each instance of the local constant with unique (not pretty) name `n` in `e` with a de-Bruijn variable. -/ meta constant expr.abstract_local : expr → name → expr diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp index c677c2c803..9c5e88efdc 100644 --- a/src/library/vm/vm_expr.cpp +++ b/src/library/vm/vm_expr.cpp @@ -237,7 +237,7 @@ vm_obj expr_lex_lt(vm_obj const & o1, vm_obj const & o2) { return mk_vm_bool(is_lt(to_expr(o1), to_expr(o2), false)); } -vm_obj expr_fold(vm_obj const &, vm_obj const & e, vm_obj const & a, vm_obj const & fn) { +vm_obj expr_fold(vm_obj const &, vm_obj const &, vm_obj const & e, vm_obj const & a, vm_obj const & fn) { vm_obj r = a; for_each(to_expr(e), [&](expr const & o, unsigned d) { r = invoke(fn, to_obj(o), mk_vm_nat(d), r); @@ -246,7 +246,7 @@ vm_obj expr_fold(vm_obj const &, vm_obj const & e, vm_obj const & a, vm_obj cons return r; } -vm_obj expr_replace(vm_obj const & e, vm_obj const & fn) { +vm_obj expr_replace(vm_obj const &, vm_obj const & e, vm_obj const & fn) { expr r = replace(to_expr(e), [&](expr const & o, unsigned d) { vm_obj new_o = invoke(fn, to_obj(o), mk_vm_nat(d)); if (is_none(new_o)) diff --git a/tests/lean/eqn_api.lean b/tests/lean/eqn_api.lean index da396133b4..755a301e5d 100644 --- a/tests/lean/eqn_api.lean +++ b/tests/lean/eqn_api.lean @@ -14,16 +14,23 @@ def all : bool -> bool -> bool -> bool -> bool open tactic +meta def replace_internal_name (e : pexpr) : pexpr := +expr.replace e $ λ e i, +match e with +| expr.const (name.mk_numeral _ _) ls := some $ expr.const `_ ls +| _ := none +end + run_cmd do e ← get_env, trace "foo", - environment.defn_spec e ``foo >>= trace, + environment.defn_spec e ``foo >>= trace ∘ replace_internal_name, trace "foo_bar", - environment.defn_spec e ``foo_bar >>= trace, + environment.defn_spec e ``foo_bar >>= trace ∘ replace_internal_name, trace "all", - environment.defn_spec e ``all >>= trace, + environment.defn_spec e ``all >>= trace ∘ replace_internal_name, trace "f", - environment.defn_spec e ``f >>= trace, + environment.defn_spec e ``f >>= trace ∘ replace_internal_name, trace "g", - environment.defn_spec e ``g >>= trace, + environment.defn_spec e ``g >>= trace ∘ replace_internal_name, skip diff --git a/tests/lean/eqn_api.lean.expected.out b/tests/lean/eqn_api.lean.expected.out index ea0942d8e7..98b70a7311 100644 --- a/tests/lean/eqn_api.lean.expected.out +++ b/tests/lean/eqn_api.lean.expected.out @@ -2,11 +2,11 @@ eqn_api.lean:17:0: error: failed state: ⊢ true foo -equations (fun (foo : (option a) -> a), (equation ((«@» foo) option.none) x)) (fun (foo : (option a) -> a) (y : 4._.15), (equation ((«@» foo) (option.some y)) y)) +equations (fun (foo : (option a) -> a), (equation ((«@» foo) option.none) x)) (fun (foo : (option a) -> a) (y : _), (equation ((«@» foo) (option.some y)) y)) foo_bar -equations (fun (foo_bar : (option a) -> a), (equation ((«@» foo_bar) option.none) x)) (fun (foo_bar : (option a) -> a) (y : 4._.21), (equation ((«@» foo_bar) (option.some y)) y)) +equations (fun (foo_bar : (option a) -> a), (equation ((«@» foo_bar) option.none) x)) (fun (foo_bar : (option a) -> a) (y : _), (equation ((«@» foo_bar) (option.some y)) y)) all -equations (fun (all : bool -> bool -> bool -> bool -> bool) (_x : 4._.4) (_x_1 : 4._.5) (_x_2 : 4._.6), (equation ((«@» all) bool.ff _x _x_1 _x_2) bool.ff)) (fun (all : bool -> bool -> bool -> bool -> bool) (_x : 4._.11) (_x_1 : 4._.12) (_x_2 : 4._.13), (equation ((«@» all) _x bool.ff _x_1 _x_2) bool.ff)) (fun (all : bool -> bool -> bool -> bool -> bool) (_x : 4._.18) (_x_1 : 4._.19) (_x_2 : 4._.20), (equation ((«@» all) _x _x_1 bool.ff _x_2) bool.ff)) (fun (all : bool -> bool -> bool -> bool -> bool) (_x : 4._.25) (_x_1 : 4._.26) (_x_2 : 4._.27), (equation ((«@» all) _x _x_1 _x_2 bool.ff) bool.ff)) (fun (all : bool -> bool -> bool -> bool -> bool) (_x : 4._.32) (_x_1 : 4._.33) (_x_2 : 4._.34) (_x_3 : 4._.35), (equation ((«@» all) _x _x_1 _x_2 _x_3) bool.tt)) +equations (fun (all : bool -> bool -> bool -> bool -> bool) (_x : _) (_x_1 : _) (_x_2 : _), (equation ((«@» all) bool.ff _x _x_1 _x_2) bool.ff)) (fun (all : bool -> bool -> bool -> bool -> bool) (_x : _) (_x_1 : _) (_x_2 : _), (equation ((«@» all) _x bool.ff _x_1 _x_2) bool.ff)) (fun (all : bool -> bool -> bool -> bool -> bool) (_x : 4._.18) (_x_1 : _) (_x_2 : _), (equation ((«@» all) _x _x_1 bool.ff _x_2) bool.ff)) (fun (all : bool -> bool -> bool -> bool -> bool) (_x : _) (_x_1 : _) (_x_2 : _), (equation ((«@» all) _x _x_1 _x_2 bool.ff) bool.ff)) (fun (all : bool -> bool -> bool -> bool -> bool) (_x : _) (_x_1 : _) (_x_2 : _) (_x_3 : _), (equation ((«@» all) _x _x_1 _x_2 _x_3) bool.tt)) f -equations (fun (f : (list nat) -> nat) (g : (list nat) -> nat), (equation ((«@» f) list.nil) 0)) (fun (f : (list nat) -> nat) (g : (list nat) -> nat) (x : 4._.2) (xs : 4._.3), (equation ((«@» f) (list.cons x xs)) (has_add.add x (g xs)))) (fun (f : (list nat) -> nat) (g : (list nat) -> nat), (equation ((«@» g) list.nil) 0)) (fun (f : (list nat) -> nat) (g : (list nat) -> nat) (x : 4._.6) (xs : 4._.7), (equation ((«@» g) (list.cons x xs)) (f xs))) +equations (fun (f : (list nat) -> nat) (g : (list nat) -> nat), (equation ((«@» f) list.nil) 0)) (fun (f : (list nat) -> nat) (g : (list nat) -> nat) (x : _) (xs : _), (equation ((«@» f) (list.cons x xs)) (has_add.add x (g xs)))) (fun (f : (list nat) -> nat) (g : (list nat) -> nat), (equation ((«@» g) list.nil) 0)) (fun (f : (list nat) -> nat) (g : (list nat) -> nat) (x : _) (xs : _), (equation ((«@» g) (list.cons x xs)) (f xs))) g From f4d38bbf77eddbf7a5b5a1aa3be599880d1c59ec Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Thu, 16 Jul 2020 19:55:47 -0400 Subject: [PATCH 3/3] fix test --- tests/lean/eqn_api.lean.expected.out | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/lean/eqn_api.lean.expected.out b/tests/lean/eqn_api.lean.expected.out index 98b70a7311..0910b57cec 100644 --- a/tests/lean/eqn_api.lean.expected.out +++ b/tests/lean/eqn_api.lean.expected.out @@ -1,4 +1,4 @@ -eqn_api.lean:17:0: error: failed +eqn_api.lean:24:0: error: failed state: ⊢ true foo @@ -6,7 +6,7 @@ equations (fun (foo : (option a) -> a), (equation ((«@» foo) option.none) x)) foo_bar equations (fun (foo_bar : (option a) -> a), (equation ((«@» foo_bar) option.none) x)) (fun (foo_bar : (option a) -> a) (y : _), (equation ((«@» foo_bar) (option.some y)) y)) all -equations (fun (all : bool -> bool -> bool -> bool -> bool) (_x : _) (_x_1 : _) (_x_2 : _), (equation ((«@» all) bool.ff _x _x_1 _x_2) bool.ff)) (fun (all : bool -> bool -> bool -> bool -> bool) (_x : _) (_x_1 : _) (_x_2 : _), (equation ((«@» all) _x bool.ff _x_1 _x_2) bool.ff)) (fun (all : bool -> bool -> bool -> bool -> bool) (_x : 4._.18) (_x_1 : _) (_x_2 : _), (equation ((«@» all) _x _x_1 bool.ff _x_2) bool.ff)) (fun (all : bool -> bool -> bool -> bool -> bool) (_x : _) (_x_1 : _) (_x_2 : _), (equation ((«@» all) _x _x_1 _x_2 bool.ff) bool.ff)) (fun (all : bool -> bool -> bool -> bool -> bool) (_x : _) (_x_1 : _) (_x_2 : _) (_x_3 : _), (equation ((«@» all) _x _x_1 _x_2 _x_3) bool.tt)) +equations (fun (all : bool -> bool -> bool -> bool -> bool) (_x : _) (_x_1 : _) (_x_2 : _), (equation ((«@» all) bool.ff _x _x_1 _x_2) bool.ff)) (fun (all : bool -> bool -> bool -> bool -> bool) (_x : _) (_x_1 : _) (_x_2 : _), (equation ((«@» all) _x bool.ff _x_1 _x_2) bool.ff)) (fun (all : bool -> bool -> bool -> bool -> bool) (_x : _) (_x_1 : _) (_x_2 : _), (equation ((«@» all) _x _x_1 bool.ff _x_2) bool.ff)) (fun (all : bool -> bool -> bool -> bool -> bool) (_x : _) (_x_1 : _) (_x_2 : _), (equation ((«@» all) _x _x_1 _x_2 bool.ff) bool.ff)) (fun (all : bool -> bool -> bool -> bool -> bool) (_x : _) (_x_1 : _) (_x_2 : _) (_x_3 : _), (equation ((«@» all) _x _x_1 _x_2 _x_3) bool.tt)) f equations (fun (f : (list nat) -> nat) (g : (list nat) -> nat), (equation ((«@» f) list.nil) 0)) (fun (f : (list nat) -> nat) (g : (list nat) -> nat) (x : _) (xs : _), (equation ((«@» f) (list.cons x xs)) (has_add.add x (g xs)))) (fun (f : (list nat) -> nat) (g : (list nat) -> nat), (equation ((«@» g) list.nil) 0)) (fun (f : (list nat) -> nat) (g : (list nat) -> nat) (x : _) (xs : _), (equation ((«@» g) (list.cons x xs)) (f xs))) g