// Lean compiler output
// Module: Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
// Imports: public import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
#ifdef __cplusplus
extern "C" {
#endif
lean_object* l_Lean_mkIntLit(lean_object*);
lean_object* l_Lean_Expr_app___override(lean_object*, lean_object*);
extern lean_object* l_Lean_instInhabitedExpr;
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_outOfBounds___redArg(lean_object*);
lean_object* l_Lean_PersistentArray_get_x21___redArg(lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_abs(lean_object*);
lean_object* l_Lean_mkRawNatLit(lean_object*);
lean_object* l_Lean_Name_mkStr1(lean_object*);
lean_object* l_Lean_Name_mkStr2(lean_object*, lean_object*);
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
lean_object* l_Lean_mkApp3(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_to_int(lean_object*);
uint8_t lean_int_dec_lt(lean_object*, lean_object*);
lean_object* l_Lean_Meta_Grind_Arith_CommRing_getNegFn___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_mkStr4(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkAppB(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_synthInstance_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkNatLit(lean_object*);
lean_object* l_Lean_Meta_Grind_Arith_CommRing_getNatCastFn___redArg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Grind_Arith_CommRing_getIntCastFn___redArg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Grind_Arith_CommRing_getAddFn___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Grind_Arith_CommRing_getSubFn___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Grind_Arith_CommRing_getMulFn___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Grind_Arith_CommRing_getPowFn___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Level_succ___override(lean_object*);
uint8_t lean_int_dec_eq(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* lean_array_get_borrowed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Grind_Arith_CommRing_PolyDerivation_p(lean_object*);
lean_object* l_Lean_mkNot(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__0(lean_object*, lean_object*, lean_object*);
static const lean_string_object l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__1___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 6, .m_capacity = 6, .m_length = 5, .m_data = "ofNat"};
static const lean_object* l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__1___closed__0 = (const lean_object*)&l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__1___closed__0_value;
static lean_once_cell_t l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__1___closed__1_once = LEAN_ONCE_CELL_INITIALIZER;
static lean_object* l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__1___closed__1;
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__2(lean_object*, lean_object*);
static const lean_string_object l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__4___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 5, .m_capacity = 5, .m_length = 4, .m_data = "Lean"};
static const lean_object* l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__4___closed__0 = (const lean_object*)&l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__4___closed__0_value;
static const lean_string_object l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__4___closed__1_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 6, .m_capacity = 6, .m_length = 5, .m_data = "Grind"};
static const lean_object* l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__4___closed__1 = (const lean_object*)&l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__4___closed__1_value;
static const lean_string_object l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__4___closed__2_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 9, .m_capacity = 9, .m_length = 8, .m_data = "Semiring"};
static const lean_object* l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__4___closed__2 = (const lean_object*)&l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__4___closed__2_value;
static const lean_ctor_object l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__4___closed__3_value_aux_0 = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 8, .m_other = 2, .m_tag = 1}, .m_objs = {((lean_object*)(((size_t)(0) << 1) | 1)),((lean_object*)&l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__4___closed__0_value),LEAN_SCALAR_PTR_LITERAL(70, 193, 83, 126, 233, 67, 208, 165)}};
static const lean_ctor_object l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__4___closed__3_value_aux_1 = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 8, .m_other = 2, .m_tag = 1}, .m_objs = {((lean_object*)&l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__4___closed__3_value_aux_0),((lean_object*)&l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__4___closed__1_value),LEAN_SCALAR_PTR_LITERAL(116, 4, 170, 185, 29, 24, 60, 188)}};
static const lean_ctor_object l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__4___closed__3_value_aux_2 = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 8, .m_other = 2, .m_tag = 1}, .m_objs = {((lean_object*)&l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__4___closed__3_value_aux_1),((lean_object*)&l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__4___closed__2_value),LEAN_SCALAR_PTR_LITERAL(246, 150, 10, 46, 185, 54, 59, 167)}};
static const lean_ctor_object l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__4___closed__3_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 8, .m_other = 2, .m_tag = 1}, .m_objs = {((lean_object*)&l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__4___closed__3_value_aux_2),((lean_object*)&l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__1___closed__0_value),LEAN_SCALAR_PTR_LITERAL(103, 49, 23, 61, 125, 46, 165, 129)}};
static const lean_object* l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__4___closed__3 = (const lean_object*)&l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__4___closed__3_value;
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static const lean_string_object l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__3___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 6, .m_capacity = 6, .m_length = 5, .m_data = "OfNat"};
static const lean_object* l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__3___closed__0 = (const lean_object*)&l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__3___closed__0_value;
static const lean_ctor_object l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__3___closed__1_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 8, .m_other = 2, .m_tag = 1}, .m_objs = {((lean_object*)(((size_t)(0) << 1) | 1)),((lean_object*)&l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__3___closed__0_value),LEAN_SCALAR_PTR_LITERAL(135, 241, 166, 108, 243, 216, 193, 244)}};
static const lean_object* l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__3___closed__1 = (const lean_object*)&l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__3___closed__1_value;
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_denoteNum(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Power_denoteExpr___redArg___lam__0(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Power_denoteExpr___redArg___lam__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Power_denoteExpr___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Power_denoteExpr(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Mon_denoteExpr_go___redArg___lam__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Mon_denoteExpr_go___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Mon_denoteExpr_go___redArg___lam__0(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Mon_denoteExpr_go(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Mon_denoteExpr___redArg___lam__0(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_once_cell_t l_Lean_Grind_CommRing_Mon_denoteExpr___redArg___closed__0_once = LEAN_ONCE_CELL_INITIALIZER;
static lean_object* l_Lean_Grind_CommRing_Mon_denoteExpr___redArg___closed__0;
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Mon_denoteExpr___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Mon_denoteExpr(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_denoteTerm___redArg___lam__0(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_denoteTerm___redArg___lam__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_denoteTerm___redArg___lam__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_denoteTerm___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_denoteTerm(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_go___redArg___lam__0(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_go___redArg___lam__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_go___redArg___lam__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_go___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_go___redArg___lam__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_go(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Poly_denoteExpr___redArg___lam__0(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Poly_denoteExpr___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Poly_denoteExpr(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__0(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__1___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__2(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__13(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__4(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Expr_denoteExpr___redArg___lam__0(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Expr_denoteExpr___redArg___lam__0___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Expr_denoteExpr___redArg___lam__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Expr_denoteExpr___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Expr_denoteExpr(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Expr_denoteExpr_x27___redArg___lam__0(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Expr_denoteExpr_x27___redArg___lam__0___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Expr_denoteExpr_x27___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Expr_denoteExpr_x27(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static const lean_string_object l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_mkEq___redArg___lam__0___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 3, .m_capacity = 3, .m_length = 2, .m_data = "Eq"};
static const lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_mkEq___redArg___lam__0___closed__0 = (const lean_object*)&l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_mkEq___redArg___lam__0___closed__0_value;
static const lean_ctor_object l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_mkEq___redArg___lam__0___closed__1_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 8, .m_other = 2, .m_tag = 1}, .m_objs = {((lean_object*)(((size_t)(0) << 1) | 1)),((lean_object*)&l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_mkEq___redArg___lam__0___closed__0_value),LEAN_SCALAR_PTR_LITERAL(143, 37, 101, 248, 9, 246, 191, 223)}};
static const lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_mkEq___redArg___lam__0___closed__1 = (const lean_object*)&l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_mkEq___redArg___lam__0___closed__1_value;
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_mkEq___redArg___lam__0(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_mkEq___redArg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_mkEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_EqCnstr_denoteExpr___redArg___lam__0(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_EqCnstr_denoteExpr___redArg___lam__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_EqCnstr_denoteExpr___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_EqCnstr_denoteExpr(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_PolyDerivation_denoteExpr___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_PolyDerivation_denoteExpr___redArg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_PolyDerivation_denoteExpr(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_PolyDerivation_denoteExpr___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_DiseqCnstr_denoteExpr___redArg___lam__0(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_DiseqCnstr_denoteExpr___redArg___lam__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_DiseqCnstr_denoteExpr___redArg___lam__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_DiseqCnstr_denoteExpr___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_DiseqCnstr_denoteExpr___redArg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_DiseqCnstr_denoteExpr(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_DiseqCnstr_denoteExpr___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__0(lean_object* v_n_1_, lean_object* v_toPure_2_, lean_object* v_____do__lift_3_){
_start:
{
lean_object* v___x_4_; lean_object* v___x_5_; 
v___x_4_ = l_Lean_Expr_app___override(v_____do__lift_3_, v_n_1_);
v___x_5_ = lean_apply_2(v_toPure_2_, lean_box(0), v___x_4_);
return v___x_5_;
}
}
static lean_object* _init_l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__1___closed__1(void){
_start:
{
lean_object* v___x_7_; lean_object* v___x_8_; 
v___x_7_ = lean_unsigned_to_nat(0u);
v___x_8_ = lean_nat_to_int(v___x_7_);
return v___x_8_;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__1(lean_object* v___x_9_, lean_object* v___x_10_, lean_object* v_type_11_, lean_object* v_n_12_, lean_object* v_k_13_, lean_object* v_toPure_14_, lean_object* v_inst_15_, lean_object* v_inst_16_, lean_object* v_inst_17_, lean_object* v_inst_18_, lean_object* v_inst_19_, lean_object* v_toBind_20_, lean_object* v_ofNatInst_21_){
_start:
{
lean_object* v___x_22_; lean_object* v___x_23_; lean_object* v___x_24_; lean_object* v_n_25_; lean_object* v___x_26_; uint8_t v___x_27_; 
v___x_22_ = ((lean_object*)(l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__1___closed__0));
v___x_23_ = l_Lean_Name_mkStr2(v___x_9_, v___x_22_);
v___x_24_ = l_Lean_mkConst(v___x_23_, v___x_10_);
v_n_25_ = l_Lean_mkApp3(v___x_24_, v_type_11_, v_n_12_, v_ofNatInst_21_);
v___x_26_ = lean_obj_once(&l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__1___closed__1, &l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__1___closed__1_once, _init_l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__1___closed__1);
v___x_27_ = lean_int_dec_lt(v_k_13_, v___x_26_);
if (v___x_27_ == 0)
{
lean_object* v___x_28_; 
lean_dec(v_toBind_20_);
lean_dec_ref(v_inst_19_);
lean_dec_ref(v_inst_18_);
lean_dec_ref(v_inst_17_);
lean_dec_ref(v_inst_16_);
lean_dec(v_inst_15_);
v___x_28_ = lean_apply_2(v_toPure_14_, lean_box(0), v_n_25_);
return v___x_28_;
}
else
{
lean_object* v___f_29_; lean_object* v___x_30_; lean_object* v___x_31_; 
v___f_29_ = lean_alloc_closure((void*)(l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__0), 3, 2);
lean_closure_set(v___f_29_, 0, v_n_25_);
lean_closure_set(v___f_29_, 1, v_toPure_14_);
v___x_30_ = l_Lean_Meta_Grind_Arith_CommRing_getNegFn___redArg(v_inst_15_, v_inst_16_, v_inst_17_, v_inst_18_, v_inst_19_);
v___x_31_ = lean_apply_4(v_toBind_20_, lean_box(0), lean_box(0), v___x_30_, v___f_29_);
return v___x_31_;
}
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__1___boxed(lean_object* v___x_32_, lean_object* v___x_33_, lean_object* v_type_34_, lean_object* v_n_35_, lean_object* v_k_36_, lean_object* v_toPure_37_, lean_object* v_inst_38_, lean_object* v_inst_39_, lean_object* v_inst_40_, lean_object* v_inst_41_, lean_object* v_inst_42_, lean_object* v_toBind_43_, lean_object* v_ofNatInst_44_){
_start:
{
lean_object* v_res_45_; 
v_res_45_ = l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__1(v___x_32_, v___x_33_, v_type_34_, v_n_35_, v_k_36_, v_toPure_37_, v_inst_38_, v_inst_39_, v_inst_40_, v_inst_41_, v_inst_42_, v_toBind_43_, v_ofNatInst_44_);
lean_dec(v_k_36_);
return v_res_45_;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__2(lean_object* v___f_46_, lean_object* v_ofNatInst_47_){
_start:
{
lean_object* v___x_48_; 
v___x_48_ = lean_apply_1(v___f_46_, v_ofNatInst_47_);
return v___x_48_;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__4(lean_object* v_toPure_57_, lean_object* v_toBind_58_, lean_object* v___f_59_, lean_object* v___x_60_, lean_object* v_type_61_, lean_object* v_semiringInst_62_, lean_object* v_n_63_, lean_object* v___f_64_, lean_object* v_____do__lift_65_){
_start:
{
if (lean_obj_tag(v_____do__lift_65_) == 1)
{
lean_object* v_val_66_; lean_object* v___x_67_; lean_object* v___x_68_; 
lean_dec(v___f_64_);
lean_dec_ref(v_n_63_);
lean_dec_ref(v_semiringInst_62_);
lean_dec_ref(v_type_61_);
lean_dec(v___x_60_);
v_val_66_ = lean_ctor_get(v_____do__lift_65_, 0);
lean_inc(v_val_66_);
lean_dec_ref(v_____do__lift_65_);
v___x_67_ = lean_apply_2(v_toPure_57_, lean_box(0), v_val_66_);
v___x_68_ = lean_apply_4(v_toBind_58_, lean_box(0), lean_box(0), v___x_67_, v___f_59_);
return v___x_68_;
}
else
{
lean_object* v___x_69_; lean_object* v___x_70_; lean_object* v___x_71_; lean_object* v___x_72_; lean_object* v___x_73_; 
lean_dec(v_____do__lift_65_);
lean_dec(v___f_59_);
v___x_69_ = ((lean_object*)(l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__4___closed__3));
v___x_70_ = l_Lean_mkConst(v___x_69_, v___x_60_);
v___x_71_ = l_Lean_mkApp3(v___x_70_, v_type_61_, v_semiringInst_62_, v_n_63_);
v___x_72_ = lean_apply_2(v_toPure_57_, lean_box(0), v___x_71_);
v___x_73_ = lean_apply_4(v_toBind_58_, lean_box(0), lean_box(0), v___x_72_, v___f_64_);
return v___x_73_;
}
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__3(lean_object* v_k_77_, lean_object* v_toPure_78_, lean_object* v_inst_79_, lean_object* v_inst_80_, lean_object* v_inst_81_, lean_object* v_inst_82_, lean_object* v_inst_83_, lean_object* v_toBind_84_, lean_object* v_ring_85_){
_start:
{
lean_object* v_type_86_; lean_object* v_u_87_; lean_object* v_semiringInst_88_; lean_object* v___x_89_; lean_object* v_n_90_; lean_object* v___x_91_; lean_object* v___x_92_; lean_object* v___x_93_; lean_object* v___x_94_; lean_object* v___f_95_; lean_object* v___f_96_; lean_object* v___f_97_; lean_object* v___x_98_; lean_object* v___x_99_; lean_object* v___x_100_; lean_object* v___x_101_; lean_object* v___x_102_; lean_object* v___x_103_; 
v_type_86_ = lean_ctor_get(v_ring_85_, 1);
lean_inc_ref(v_type_86_);
v_u_87_ = lean_ctor_get(v_ring_85_, 2);
lean_inc(v_u_87_);
v_semiringInst_88_ = lean_ctor_get(v_ring_85_, 4);
lean_inc_ref(v_semiringInst_88_);
lean_dec_ref(v_ring_85_);
v___x_89_ = lean_nat_abs(v_k_77_);
v_n_90_ = l_Lean_mkRawNatLit(v___x_89_);
v___x_91_ = ((lean_object*)(l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__3___closed__0));
v___x_92_ = ((lean_object*)(l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__3___closed__1));
v___x_93_ = lean_box(0);
v___x_94_ = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(v___x_94_, 0, v_u_87_);
lean_ctor_set(v___x_94_, 1, v___x_93_);
lean_inc(v_toBind_84_);
lean_inc(v_inst_79_);
lean_inc(v_toPure_78_);
lean_inc_ref(v_n_90_);
lean_inc_ref(v_type_86_);
lean_inc_ref(v___x_94_);
v___f_95_ = lean_alloc_closure((void*)(l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__1___boxed), 13, 12);
lean_closure_set(v___f_95_, 0, v___x_91_);
lean_closure_set(v___f_95_, 1, v___x_94_);
lean_closure_set(v___f_95_, 2, v_type_86_);
lean_closure_set(v___f_95_, 3, v_n_90_);
lean_closure_set(v___f_95_, 4, v_k_77_);
lean_closure_set(v___f_95_, 5, v_toPure_78_);
lean_closure_set(v___f_95_, 6, v_inst_79_);
lean_closure_set(v___f_95_, 7, v_inst_80_);
lean_closure_set(v___f_95_, 8, v_inst_81_);
lean_closure_set(v___f_95_, 9, v_inst_82_);
lean_closure_set(v___f_95_, 10, v_inst_83_);
lean_closure_set(v___f_95_, 11, v_toBind_84_);
v___f_96_ = lean_alloc_closure((void*)(l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__2), 2, 1);
lean_closure_set(v___f_96_, 0, v___f_95_);
lean_inc_ref(v_n_90_);
lean_inc_ref(v_type_86_);
lean_inc_ref(v___x_94_);
lean_inc_ref(v___f_96_);
lean_inc(v_toBind_84_);
v___f_97_ = lean_alloc_closure((void*)(l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__4), 9, 8);
lean_closure_set(v___f_97_, 0, v_toPure_78_);
lean_closure_set(v___f_97_, 1, v_toBind_84_);
lean_closure_set(v___f_97_, 2, v___f_96_);
lean_closure_set(v___f_97_, 3, v___x_94_);
lean_closure_set(v___f_97_, 4, v_type_86_);
lean_closure_set(v___f_97_, 5, v_semiringInst_88_);
lean_closure_set(v___f_97_, 6, v_n_90_);
lean_closure_set(v___f_97_, 7, v___f_96_);
v___x_98_ = l_Lean_mkConst(v___x_92_, v___x_94_);
v___x_99_ = l_Lean_mkAppB(v___x_98_, v_type_86_, v_n_90_);
v___x_100_ = lean_box(0);
v___x_101_ = lean_alloc_closure((void*)(l_Lean_Meta_synthInstance_x3f___boxed), 7, 2);
lean_closure_set(v___x_101_, 0, v___x_99_);
lean_closure_set(v___x_101_, 1, v___x_100_);
v___x_102_ = lean_apply_2(v_inst_79_, lean_box(0), v___x_101_);
v___x_103_ = lean_apply_4(v_toBind_84_, lean_box(0), lean_box(0), v___x_102_, v___f_97_);
return v___x_103_;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg(lean_object* v_inst_104_, lean_object* v_inst_105_, lean_object* v_inst_106_, lean_object* v_inst_107_, lean_object* v_inst_108_, lean_object* v_k_109_){
_start:
{
lean_object* v_toApplicative_110_; lean_object* v_toBind_111_; lean_object* v_getRing_112_; lean_object* v_toPure_113_; lean_object* v___f_114_; lean_object* v___x_115_; 
v_toApplicative_110_ = lean_ctor_get(v_inst_104_, 0);
v_toBind_111_ = lean_ctor_get(v_inst_104_, 1);
lean_inc(v_toBind_111_);
v_getRing_112_ = lean_ctor_get(v_inst_108_, 0);
lean_inc(v_getRing_112_);
v_toPure_113_ = lean_ctor_get(v_toApplicative_110_, 1);
lean_inc(v_toPure_113_);
lean_inc(v_toBind_111_);
v___f_114_ = lean_alloc_closure((void*)(l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__3), 9, 8);
lean_closure_set(v___f_114_, 0, v_k_109_);
lean_closure_set(v___f_114_, 1, v_toPure_113_);
lean_closure_set(v___f_114_, 2, v_inst_106_);
lean_closure_set(v___f_114_, 3, v_inst_105_);
lean_closure_set(v___f_114_, 4, v_inst_104_);
lean_closure_set(v___f_114_, 5, v_inst_107_);
lean_closure_set(v___f_114_, 6, v_inst_108_);
lean_closure_set(v___f_114_, 7, v_toBind_111_);
v___x_115_ = lean_apply_4(v_toBind_111_, lean_box(0), lean_box(0), v_getRing_112_, v___f_114_);
return v___x_115_;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_denoteNum(lean_object* v_M_116_, lean_object* v_inst_117_, lean_object* v_inst_118_, lean_object* v_inst_119_, lean_object* v_inst_120_, lean_object* v_inst_121_, lean_object* v_k_122_){
_start:
{
lean_object* v___x_123_; 
v___x_123_ = l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg(v_inst_117_, v_inst_118_, v_inst_119_, v_inst_120_, v_inst_121_, v_k_122_);
return v___x_123_;
}
}
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Power_denoteExpr___redArg___lam__0(lean_object* v_toApplicative_124_, lean_object* v_k_125_, lean_object* v___y_126_, lean_object* v_____do__lift_127_){
_start:
{
lean_object* v_toPure_128_; lean_object* v___x_129_; lean_object* v___x_130_; lean_object* v___x_131_; 
v_toPure_128_ = lean_ctor_get(v_toApplicative_124_, 1);
lean_inc(v_toPure_128_);
lean_dec_ref(v_toApplicative_124_);
v___x_129_ = l_Lean_mkNatLit(v_k_125_);
v___x_130_ = l_Lean_mkAppB(v_____do__lift_127_, v___y_126_, v___x_129_);
v___x_131_ = lean_apply_2(v_toPure_128_, lean_box(0), v___x_130_);
return v___x_131_;
}
}
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Power_denoteExpr___redArg___lam__1(lean_object* v_pw_132_, lean_object* v_toApplicative_133_, lean_object* v_inst_134_, lean_object* v_inst_135_, lean_object* v_inst_136_, lean_object* v_inst_137_, lean_object* v_inst_138_, lean_object* v_toBind_139_, lean_object* v___x_140_, lean_object* v_____do__lift_141_){
_start:
{
lean_object* v_vars_142_; lean_object* v_x_143_; lean_object* v_k_144_; lean_object* v___y_146_; lean_object* v_size_154_; uint8_t v___x_155_; 
v_vars_142_ = lean_ctor_get(v_____do__lift_141_, 14);
lean_inc_ref(v_vars_142_);
lean_dec_ref(v_____do__lift_141_);
v_x_143_ = lean_ctor_get(v_pw_132_, 0);
lean_inc(v_x_143_);
v_k_144_ = lean_ctor_get(v_pw_132_, 1);
lean_inc(v_k_144_);
lean_dec_ref(v_pw_132_);
v_size_154_ = lean_ctor_get(v_vars_142_, 2);
v___x_155_ = lean_nat_dec_lt(v_x_143_, v_size_154_);
if (v___x_155_ == 0)
{
lean_object* v___x_156_; 
lean_dec(v_x_143_);
lean_dec_ref(v_vars_142_);
v___x_156_ = l_outOfBounds___redArg(v___x_140_);
v___y_146_ = v___x_156_;
goto v___jp_145_;
}
else
{
lean_object* v___x_157_; 
v___x_157_ = l_Lean_PersistentArray_get_x21___redArg(v___x_140_, v_vars_142_, v_x_143_);
lean_dec(v_x_143_);
v___y_146_ = v___x_157_;
goto v___jp_145_;
}
v___jp_145_:
{
lean_object* v___x_147_; uint8_t v___x_148_; 
v___x_147_ = lean_unsigned_to_nat(1u);
v___x_148_ = lean_nat_dec_eq(v_k_144_, v___x_147_);
if (v___x_148_ == 0)
{
lean_object* v___f_149_; lean_object* v___x_150_; lean_object* v___x_151_; 
v___f_149_ = lean_alloc_closure((void*)(l_Lean_Grind_CommRing_Power_denoteExpr___redArg___lam__0), 4, 3);
lean_closure_set(v___f_149_, 0, v_toApplicative_133_);
lean_closure_set(v___f_149_, 1, v_k_144_);
lean_closure_set(v___f_149_, 2, v___y_146_);
v___x_150_ = l_Lean_Meta_Grind_Arith_CommRing_getPowFn___redArg(v_inst_134_, v_inst_135_, v_inst_136_, v_inst_137_, v_inst_138_);
v___x_151_ = lean_apply_4(v_toBind_139_, lean_box(0), lean_box(0), v___x_150_, v___f_149_);
return v___x_151_;
}
else
{
lean_object* v_toPure_152_; lean_object* v___x_153_; 
lean_dec(v_k_144_);
lean_dec(v_toBind_139_);
lean_dec_ref(v_inst_138_);
lean_dec_ref(v_inst_137_);
lean_dec_ref(v_inst_136_);
lean_dec_ref(v_inst_135_);
lean_dec(v_inst_134_);
v_toPure_152_ = lean_ctor_get(v_toApplicative_133_, 1);
lean_inc(v_toPure_152_);
lean_dec_ref(v_toApplicative_133_);
v___x_153_ = lean_apply_2(v_toPure_152_, lean_box(0), v___y_146_);
return v___x_153_;
}
}
}
}
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Power_denoteExpr___redArg(lean_object* v_inst_158_, lean_object* v_inst_159_, lean_object* v_inst_160_, lean_object* v_inst_161_, lean_object* v_inst_162_, lean_object* v_pw_163_){
_start:
{
lean_object* v_toApplicative_164_; lean_object* v_toBind_165_; lean_object* v_getRing_166_; lean_object* v___x_167_; lean_object* v___f_168_; lean_object* v___x_169_; 
v_toApplicative_164_ = lean_ctor_get(v_inst_158_, 0);
lean_inc_ref(v_toApplicative_164_);
v_toBind_165_ = lean_ctor_get(v_inst_158_, 1);
lean_inc(v_toBind_165_);
v_getRing_166_ = lean_ctor_get(v_inst_162_, 0);
lean_inc(v_getRing_166_);
v___x_167_ = l_Lean_instInhabitedExpr;
lean_inc(v_toBind_165_);
v___f_168_ = lean_alloc_closure((void*)(l_Lean_Grind_CommRing_Power_denoteExpr___redArg___lam__1), 10, 9);
lean_closure_set(v___f_168_, 0, v_pw_163_);
lean_closure_set(v___f_168_, 1, v_toApplicative_164_);
lean_closure_set(v___f_168_, 2, v_inst_160_);
lean_closure_set(v___f_168_, 3, v_inst_159_);
lean_closure_set(v___f_168_, 4, v_inst_158_);
lean_closure_set(v___f_168_, 5, v_inst_161_);
lean_closure_set(v___f_168_, 6, v_inst_162_);
lean_closure_set(v___f_168_, 7, v_toBind_165_);
lean_closure_set(v___f_168_, 8, v___x_167_);
v___x_169_ = lean_apply_4(v_toBind_165_, lean_box(0), lean_box(0), v_getRing_166_, v___f_168_);
return v___x_169_;
}
}
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Power_denoteExpr(lean_object* v_M_170_, lean_object* v_inst_171_, lean_object* v_inst_172_, lean_object* v_inst_173_, lean_object* v_inst_174_, lean_object* v_inst_175_, lean_object* v_pw_176_){
_start:
{
lean_object* v___x_177_; 
v___x_177_ = l_Lean_Grind_CommRing_Power_denoteExpr___redArg(v_inst_171_, v_inst_172_, v_inst_173_, v_inst_174_, v_inst_175_, v_pw_176_);
return v___x_177_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Mon_denoteExpr_go___redArg___lam__1(lean_object* v_acc_178_, lean_object* v_inst_179_, lean_object* v_inst_180_, lean_object* v_inst_181_, lean_object* v_inst_182_, lean_object* v_inst_183_, lean_object* v_m_184_, lean_object* v_p_185_, lean_object* v_toBind_186_, lean_object* v_____do__lift_187_){
_start:
{
lean_object* v___f_188_; lean_object* v___x_189_; lean_object* v___x_190_; 
lean_inc_ref(v_inst_183_);
lean_inc_ref(v_inst_182_);
lean_inc(v_inst_181_);
lean_inc_ref(v_inst_180_);
lean_inc_ref(v_inst_179_);
v___f_188_ = lean_alloc_closure((void*)(l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Mon_denoteExpr_go___redArg___lam__0), 9, 8);
lean_closure_set(v___f_188_, 0, v_____do__lift_187_);
lean_closure_set(v___f_188_, 1, v_acc_178_);
lean_closure_set(v___f_188_, 2, v_inst_179_);
lean_closure_set(v___f_188_, 3, v_inst_180_);
lean_closure_set(v___f_188_, 4, v_inst_181_);
lean_closure_set(v___f_188_, 5, v_inst_182_);
lean_closure_set(v___f_188_, 6, v_inst_183_);
lean_closure_set(v___f_188_, 7, v_m_184_);
v___x_189_ = l_Lean_Grind_CommRing_Power_denoteExpr___redArg(v_inst_179_, v_inst_180_, v_inst_181_, v_inst_182_, v_inst_183_, v_p_185_);
v___x_190_ = lean_apply_4(v_toBind_186_, lean_box(0), lean_box(0), v___x_189_, v___f_188_);
return v___x_190_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Mon_denoteExpr_go___redArg(lean_object* v_inst_191_, lean_object* v_inst_192_, lean_object* v_inst_193_, lean_object* v_inst_194_, lean_object* v_inst_195_, lean_object* v_m_196_, lean_object* v_acc_197_){
_start:
{
if (lean_obj_tag(v_m_196_) == 0)
{
lean_object* v_toApplicative_198_; lean_object* v_toPure_199_; lean_object* v___x_200_; 
v_toApplicative_198_ = lean_ctor_get(v_inst_191_, 0);
lean_inc_ref(v_toApplicative_198_);
lean_dec_ref(v_inst_195_);
lean_dec_ref(v_inst_194_);
lean_dec(v_inst_193_);
lean_dec_ref(v_inst_192_);
lean_dec_ref(v_inst_191_);
v_toPure_199_ = lean_ctor_get(v_toApplicative_198_, 1);
lean_inc(v_toPure_199_);
lean_dec_ref(v_toApplicative_198_);
v___x_200_ = lean_apply_2(v_toPure_199_, lean_box(0), v_acc_197_);
return v___x_200_;
}
else
{
lean_object* v_toBind_201_; lean_object* v_p_202_; lean_object* v_m_203_; lean_object* v___f_204_; lean_object* v___x_205_; lean_object* v___x_206_; 
v_toBind_201_ = lean_ctor_get(v_inst_191_, 1);
lean_inc(v_toBind_201_);
v_p_202_ = lean_ctor_get(v_m_196_, 0);
lean_inc_ref(v_p_202_);
v_m_203_ = lean_ctor_get(v_m_196_, 1);
lean_inc(v_m_203_);
lean_dec_ref(v_m_196_);
lean_inc(v_toBind_201_);
lean_inc_ref(v_inst_195_);
lean_inc_ref(v_inst_194_);
lean_inc(v_inst_193_);
lean_inc_ref(v_inst_192_);
lean_inc_ref(v_inst_191_);
v___f_204_ = lean_alloc_closure((void*)(l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Mon_denoteExpr_go___redArg___lam__1), 10, 9);
lean_closure_set(v___f_204_, 0, v_acc_197_);
lean_closure_set(v___f_204_, 1, v_inst_191_);
lean_closure_set(v___f_204_, 2, v_inst_192_);
lean_closure_set(v___f_204_, 3, v_inst_193_);
lean_closure_set(v___f_204_, 4, v_inst_194_);
lean_closure_set(v___f_204_, 5, v_inst_195_);
lean_closure_set(v___f_204_, 6, v_m_203_);
lean_closure_set(v___f_204_, 7, v_p_202_);
lean_closure_set(v___f_204_, 8, v_toBind_201_);
v___x_205_ = l_Lean_Meta_Grind_Arith_CommRing_getMulFn___redArg(v_inst_193_, v_inst_192_, v_inst_191_, v_inst_194_, v_inst_195_);
v___x_206_ = lean_apply_4(v_toBind_201_, lean_box(0), lean_box(0), v___x_205_, v___f_204_);
return v___x_206_;
}
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Mon_denoteExpr_go___redArg___lam__0(lean_object* v_____do__lift_207_, lean_object* v_acc_208_, lean_object* v_inst_209_, lean_object* v_inst_210_, lean_object* v_inst_211_, lean_object* v_inst_212_, lean_object* v_inst_213_, lean_object* v_m_214_, lean_object* v_____do__lift_215_){
_start:
{
lean_object* v___x_216_; lean_object* v___x_217_; 
v___x_216_ = l_Lean_mkAppB(v_____do__lift_207_, v_acc_208_, v_____do__lift_215_);
v___x_217_ = l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Mon_denoteExpr_go___redArg(v_inst_209_, v_inst_210_, v_inst_211_, v_inst_212_, v_inst_213_, v_m_214_, v___x_216_);
return v___x_217_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Mon_denoteExpr_go(lean_object* v_M_218_, lean_object* v_inst_219_, lean_object* v_inst_220_, lean_object* v_inst_221_, lean_object* v_inst_222_, lean_object* v_inst_223_, lean_object* v_m_224_, lean_object* v_acc_225_){
_start:
{
lean_object* v___x_226_; 
v___x_226_ = l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Mon_denoteExpr_go___redArg(v_inst_219_, v_inst_220_, v_inst_221_, v_inst_222_, v_inst_223_, v_m_224_, v_acc_225_);
return v___x_226_;
}
}
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Mon_denoteExpr___redArg___lam__0(lean_object* v_inst_227_, lean_object* v_inst_228_, lean_object* v_inst_229_, lean_object* v_inst_230_, lean_object* v_inst_231_, lean_object* v_m_232_, lean_object* v_____do__lift_233_){
_start:
{
lean_object* v___x_234_; 
v___x_234_ = l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Mon_denoteExpr_go___redArg(v_inst_227_, v_inst_228_, v_inst_229_, v_inst_230_, v_inst_231_, v_m_232_, v_____do__lift_233_);
return v___x_234_;
}
}
static lean_object* _init_l_Lean_Grind_CommRing_Mon_denoteExpr___redArg___closed__0(void){
_start:
{
lean_object* v___x_235_; lean_object* v___x_236_; 
v___x_235_ = lean_unsigned_to_nat(1u);
v___x_236_ = lean_nat_to_int(v___x_235_);
return v___x_236_;
}
}
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Mon_denoteExpr___redArg(lean_object* v_inst_237_, lean_object* v_inst_238_, lean_object* v_inst_239_, lean_object* v_inst_240_, lean_object* v_inst_241_, lean_object* v_m_242_){
_start:
{
if (lean_obj_tag(v_m_242_) == 0)
{
lean_object* v___x_243_; lean_object* v___x_244_; 
v___x_243_ = lean_obj_once(&l_Lean_Grind_CommRing_Mon_denoteExpr___redArg___closed__0, &l_Lean_Grind_CommRing_Mon_denoteExpr___redArg___closed__0_once, _init_l_Lean_Grind_CommRing_Mon_denoteExpr___redArg___closed__0);
v___x_244_ = l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg(v_inst_237_, v_inst_238_, v_inst_239_, v_inst_240_, v_inst_241_, v___x_243_);
return v___x_244_;
}
else
{
lean_object* v_toBind_245_; lean_object* v_p_246_; lean_object* v_m_247_; lean_object* v___f_248_; lean_object* v___x_249_; lean_object* v___x_250_; 
v_toBind_245_ = lean_ctor_get(v_inst_237_, 1);
lean_inc(v_toBind_245_);
v_p_246_ = lean_ctor_get(v_m_242_, 0);
lean_inc_ref(v_p_246_);
v_m_247_ = lean_ctor_get(v_m_242_, 1);
lean_inc(v_m_247_);
lean_dec_ref(v_m_242_);
lean_inc_ref(v_inst_241_);
lean_inc_ref(v_inst_240_);
lean_inc(v_inst_239_);
lean_inc_ref(v_inst_238_);
lean_inc_ref(v_inst_237_);
v___f_248_ = lean_alloc_closure((void*)(l_Lean_Grind_CommRing_Mon_denoteExpr___redArg___lam__0), 7, 6);
lean_closure_set(v___f_248_, 0, v_inst_237_);
lean_closure_set(v___f_248_, 1, v_inst_238_);
lean_closure_set(v___f_248_, 2, v_inst_239_);
lean_closure_set(v___f_248_, 3, v_inst_240_);
lean_closure_set(v___f_248_, 4, v_inst_241_);
lean_closure_set(v___f_248_, 5, v_m_247_);
v___x_249_ = l_Lean_Grind_CommRing_Power_denoteExpr___redArg(v_inst_237_, v_inst_238_, v_inst_239_, v_inst_240_, v_inst_241_, v_p_246_);
v___x_250_ = lean_apply_4(v_toBind_245_, lean_box(0), lean_box(0), v___x_249_, v___f_248_);
return v___x_250_;
}
}
}
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Mon_denoteExpr(lean_object* v_M_251_, lean_object* v_inst_252_, lean_object* v_inst_253_, lean_object* v_inst_254_, lean_object* v_inst_255_, lean_object* v_inst_256_, lean_object* v_m_257_){
_start:
{
lean_object* v___x_258_; 
v___x_258_ = l_Lean_Grind_CommRing_Mon_denoteExpr___redArg(v_inst_252_, v_inst_253_, v_inst_254_, v_inst_255_, v_inst_256_, v_m_257_);
return v___x_258_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_denoteTerm___redArg___lam__0(lean_object* v_toApplicative_259_, lean_object* v_____do__lift_260_, lean_object* v_____do__lift_261_, lean_object* v_____do__lift_262_){
_start:
{
lean_object* v_toPure_263_; lean_object* v___x_264_; lean_object* v___x_265_; 
v_toPure_263_ = lean_ctor_get(v_toApplicative_259_, 1);
lean_inc(v_toPure_263_);
lean_dec_ref(v_toApplicative_259_);
v___x_264_ = l_Lean_mkAppB(v_____do__lift_260_, v_____do__lift_261_, v_____do__lift_262_);
v___x_265_ = lean_apply_2(v_toPure_263_, lean_box(0), v___x_264_);
return v___x_265_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_denoteTerm___redArg___lam__1(lean_object* v_toApplicative_266_, lean_object* v_____do__lift_267_, lean_object* v_inst_268_, lean_object* v_inst_269_, lean_object* v_inst_270_, lean_object* v_inst_271_, lean_object* v_inst_272_, lean_object* v_m_273_, lean_object* v_toBind_274_, lean_object* v_____do__lift_275_){
_start:
{
lean_object* v___f_276_; lean_object* v___x_277_; lean_object* v___x_278_; 
v___f_276_ = lean_alloc_closure((void*)(l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_denoteTerm___redArg___lam__0), 4, 3);
lean_closure_set(v___f_276_, 0, v_toApplicative_266_);
lean_closure_set(v___f_276_, 1, v_____do__lift_267_);
lean_closure_set(v___f_276_, 2, v_____do__lift_275_);
v___x_277_ = l_Lean_Grind_CommRing_Mon_denoteExpr___redArg(v_inst_268_, v_inst_269_, v_inst_270_, v_inst_271_, v_inst_272_, v_m_273_);
v___x_278_ = lean_apply_4(v_toBind_274_, lean_box(0), lean_box(0), v___x_277_, v___f_276_);
return v___x_278_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_denoteTerm___redArg___lam__2(lean_object* v_toApplicative_279_, lean_object* v_inst_280_, lean_object* v_inst_281_, lean_object* v_inst_282_, lean_object* v_inst_283_, lean_object* v_inst_284_, lean_object* v_m_285_, lean_object* v_toBind_286_, lean_object* v_k_287_, lean_object* v_____do__lift_288_){
_start:
{
lean_object* v___f_289_; lean_object* v___x_290_; lean_object* v___x_291_; 
lean_inc(v_toBind_286_);
lean_inc_ref(v_inst_284_);
lean_inc_ref(v_inst_283_);
lean_inc(v_inst_282_);
lean_inc_ref(v_inst_281_);
lean_inc_ref(v_inst_280_);
v___f_289_ = lean_alloc_closure((void*)(l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_denoteTerm___redArg___lam__1), 10, 9);
lean_closure_set(v___f_289_, 0, v_toApplicative_279_);
lean_closure_set(v___f_289_, 1, v_____do__lift_288_);
lean_closure_set(v___f_289_, 2, v_inst_280_);
lean_closure_set(v___f_289_, 3, v_inst_281_);
lean_closure_set(v___f_289_, 4, v_inst_282_);
lean_closure_set(v___f_289_, 5, v_inst_283_);
lean_closure_set(v___f_289_, 6, v_inst_284_);
lean_closure_set(v___f_289_, 7, v_m_285_);
lean_closure_set(v___f_289_, 8, v_toBind_286_);
v___x_290_ = l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg(v_inst_280_, v_inst_281_, v_inst_282_, v_inst_283_, v_inst_284_, v_k_287_);
v___x_291_ = lean_apply_4(v_toBind_286_, lean_box(0), lean_box(0), v___x_290_, v___f_289_);
return v___x_291_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_denoteTerm___redArg(lean_object* v_inst_292_, lean_object* v_inst_293_, lean_object* v_inst_294_, lean_object* v_inst_295_, lean_object* v_inst_296_, lean_object* v_k_297_, lean_object* v_m_298_){
_start:
{
lean_object* v___x_299_; uint8_t v___x_300_; 
v___x_299_ = lean_obj_once(&l_Lean_Grind_CommRing_Mon_denoteExpr___redArg___closed__0, &l_Lean_Grind_CommRing_Mon_denoteExpr___redArg___closed__0_once, _init_l_Lean_Grind_CommRing_Mon_denoteExpr___redArg___closed__0);
v___x_300_ = lean_int_dec_eq(v_k_297_, v___x_299_);
if (v___x_300_ == 0)
{
lean_object* v_toApplicative_301_; lean_object* v_toBind_302_; lean_object* v___f_303_; lean_object* v___x_304_; lean_object* v___x_305_; 
v_toApplicative_301_ = lean_ctor_get(v_inst_292_, 0);
v_toBind_302_ = lean_ctor_get(v_inst_292_, 1);
lean_inc(v_toBind_302_);
lean_inc(v_toBind_302_);
lean_inc_ref(v_inst_296_);
lean_inc_ref(v_inst_295_);
lean_inc(v_inst_294_);
lean_inc_ref(v_inst_293_);
lean_inc_ref(v_inst_292_);
lean_inc_ref(v_toApplicative_301_);
v___f_303_ = lean_alloc_closure((void*)(l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_denoteTerm___redArg___lam__2), 10, 9);
lean_closure_set(v___f_303_, 0, v_toApplicative_301_);
lean_closure_set(v___f_303_, 1, v_inst_292_);
lean_closure_set(v___f_303_, 2, v_inst_293_);
lean_closure_set(v___f_303_, 3, v_inst_294_);
lean_closure_set(v___f_303_, 4, v_inst_295_);
lean_closure_set(v___f_303_, 5, v_inst_296_);
lean_closure_set(v___f_303_, 6, v_m_298_);
lean_closure_set(v___f_303_, 7, v_toBind_302_);
lean_closure_set(v___f_303_, 8, v_k_297_);
v___x_304_ = l_Lean_Meta_Grind_Arith_CommRing_getMulFn___redArg(v_inst_294_, v_inst_293_, v_inst_292_, v_inst_295_, v_inst_296_);
v___x_305_ = lean_apply_4(v_toBind_302_, lean_box(0), lean_box(0), v___x_304_, v___f_303_);
return v___x_305_;
}
else
{
lean_object* v___x_306_; 
lean_dec(v_k_297_);
v___x_306_ = l_Lean_Grind_CommRing_Mon_denoteExpr___redArg(v_inst_292_, v_inst_293_, v_inst_294_, v_inst_295_, v_inst_296_, v_m_298_);
return v___x_306_;
}
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_denoteTerm(lean_object* v_M_307_, lean_object* v_inst_308_, lean_object* v_inst_309_, lean_object* v_inst_310_, lean_object* v_inst_311_, lean_object* v_inst_312_, lean_object* v_k_313_, lean_object* v_m_314_){
_start:
{
lean_object* v___x_315_; 
v___x_315_ = l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_denoteTerm___redArg(v_inst_308_, v_inst_309_, v_inst_310_, v_inst_311_, v_inst_312_, v_k_313_, v_m_314_);
return v___x_315_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_go___redArg___lam__0(lean_object* v_____do__lift_316_, lean_object* v_acc_317_, lean_object* v_toPure_318_, lean_object* v_____do__lift_319_){
_start:
{
lean_object* v___x_320_; lean_object* v___x_321_; 
v___x_320_ = l_Lean_mkAppB(v_____do__lift_316_, v_acc_317_, v_____do__lift_319_);
v___x_321_ = lean_apply_2(v_toPure_318_, lean_box(0), v___x_320_);
return v___x_321_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_go___redArg___lam__1(lean_object* v_acc_322_, lean_object* v_toPure_323_, lean_object* v_inst_324_, lean_object* v_inst_325_, lean_object* v_inst_326_, lean_object* v_inst_327_, lean_object* v_inst_328_, lean_object* v_k_329_, lean_object* v_toBind_330_, lean_object* v_____do__lift_331_){
_start:
{
lean_object* v___f_332_; lean_object* v___x_333_; lean_object* v___x_334_; 
v___f_332_ = lean_alloc_closure((void*)(l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_go___redArg___lam__0), 4, 3);
lean_closure_set(v___f_332_, 0, v_____do__lift_331_);
lean_closure_set(v___f_332_, 1, v_acc_322_);
lean_closure_set(v___f_332_, 2, v_toPure_323_);
v___x_333_ = l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg(v_inst_324_, v_inst_325_, v_inst_326_, v_inst_327_, v_inst_328_, v_k_329_);
v___x_334_ = lean_apply_4(v_toBind_330_, lean_box(0), lean_box(0), v___x_333_, v___f_332_);
return v___x_334_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_go___redArg___lam__3(lean_object* v_acc_335_, lean_object* v_inst_336_, lean_object* v_inst_337_, lean_object* v_inst_338_, lean_object* v_inst_339_, lean_object* v_inst_340_, lean_object* v_p_341_, lean_object* v_k_342_, lean_object* v_v_343_, lean_object* v_toBind_344_, lean_object* v_____do__lift_345_){
_start:
{
lean_object* v___f_346_; lean_object* v___x_347_; lean_object* v___x_348_; 
lean_inc_ref(v_inst_340_);
lean_inc_ref(v_inst_339_);
lean_inc(v_inst_338_);
lean_inc_ref(v_inst_337_);
lean_inc_ref(v_inst_336_);
v___f_346_ = lean_alloc_closure((void*)(l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_go___redArg___lam__2), 9, 8);
lean_closure_set(v___f_346_, 0, v_____do__lift_345_);
lean_closure_set(v___f_346_, 1, v_acc_335_);
lean_closure_set(v___f_346_, 2, v_inst_336_);
lean_closure_set(v___f_346_, 3, v_inst_337_);
lean_closure_set(v___f_346_, 4, v_inst_338_);
lean_closure_set(v___f_346_, 5, v_inst_339_);
lean_closure_set(v___f_346_, 6, v_inst_340_);
lean_closure_set(v___f_346_, 7, v_p_341_);
v___x_347_ = l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_denoteTerm___redArg(v_inst_336_, v_inst_337_, v_inst_338_, v_inst_339_, v_inst_340_, v_k_342_, v_v_343_);
v___x_348_ = lean_apply_4(v_toBind_344_, lean_box(0), lean_box(0), v___x_347_, v___f_346_);
return v___x_348_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_go___redArg(lean_object* v_inst_349_, lean_object* v_inst_350_, lean_object* v_inst_351_, lean_object* v_inst_352_, lean_object* v_inst_353_, lean_object* v_p_354_, lean_object* v_acc_355_){
_start:
{
if (lean_obj_tag(v_p_354_) == 0)
{
lean_object* v_toApplicative_356_; lean_object* v_toBind_357_; lean_object* v_toPure_358_; lean_object* v_k_359_; lean_object* v___x_360_; uint8_t v___x_361_; 
v_toApplicative_356_ = lean_ctor_get(v_inst_349_, 0);
v_toBind_357_ = lean_ctor_get(v_inst_349_, 1);
lean_inc(v_toBind_357_);
v_toPure_358_ = lean_ctor_get(v_toApplicative_356_, 1);
v_k_359_ = lean_ctor_get(v_p_354_, 0);
lean_inc(v_k_359_);
lean_dec_ref(v_p_354_);
v___x_360_ = lean_obj_once(&l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__1___closed__1, &l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__1___closed__1_once, _init_l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__1___closed__1);
v___x_361_ = lean_int_dec_eq(v_k_359_, v___x_360_);
if (v___x_361_ == 0)
{
lean_object* v___f_362_; lean_object* v___x_363_; lean_object* v___x_364_; 
lean_inc(v_toBind_357_);
lean_inc_ref(v_inst_353_);
lean_inc_ref(v_inst_352_);
lean_inc(v_inst_351_);
lean_inc_ref(v_inst_350_);
lean_inc_ref(v_inst_349_);
lean_inc(v_toPure_358_);
v___f_362_ = lean_alloc_closure((void*)(l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_go___redArg___lam__1), 10, 9);
lean_closure_set(v___f_362_, 0, v_acc_355_);
lean_closure_set(v___f_362_, 1, v_toPure_358_);
lean_closure_set(v___f_362_, 2, v_inst_349_);
lean_closure_set(v___f_362_, 3, v_inst_350_);
lean_closure_set(v___f_362_, 4, v_inst_351_);
lean_closure_set(v___f_362_, 5, v_inst_352_);
lean_closure_set(v___f_362_, 6, v_inst_353_);
lean_closure_set(v___f_362_, 7, v_k_359_);
lean_closure_set(v___f_362_, 8, v_toBind_357_);
v___x_363_ = l_Lean_Meta_Grind_Arith_CommRing_getAddFn___redArg(v_inst_351_, v_inst_350_, v_inst_349_, v_inst_352_, v_inst_353_);
v___x_364_ = lean_apply_4(v_toBind_357_, lean_box(0), lean_box(0), v___x_363_, v___f_362_);
return v___x_364_;
}
else
{
lean_object* v___x_365_; 
lean_inc(v_toPure_358_);
lean_dec(v_k_359_);
lean_dec(v_toBind_357_);
lean_dec_ref(v_inst_353_);
lean_dec_ref(v_inst_352_);
lean_dec(v_inst_351_);
lean_dec_ref(v_inst_350_);
lean_dec_ref(v_inst_349_);
v___x_365_ = lean_apply_2(v_toPure_358_, lean_box(0), v_acc_355_);
return v___x_365_;
}
}
else
{
lean_object* v_toBind_366_; lean_object* v_k_367_; lean_object* v_v_368_; lean_object* v_p_369_; lean_object* v___f_370_; lean_object* v___x_371_; lean_object* v___x_372_; 
v_toBind_366_ = lean_ctor_get(v_inst_349_, 1);
lean_inc(v_toBind_366_);
v_k_367_ = lean_ctor_get(v_p_354_, 0);
lean_inc(v_k_367_);
v_v_368_ = lean_ctor_get(v_p_354_, 1);
lean_inc(v_v_368_);
v_p_369_ = lean_ctor_get(v_p_354_, 2);
lean_inc_ref(v_p_369_);
lean_dec_ref(v_p_354_);
lean_inc(v_toBind_366_);
lean_inc_ref(v_inst_353_);
lean_inc_ref(v_inst_352_);
lean_inc(v_inst_351_);
lean_inc_ref(v_inst_350_);
lean_inc_ref(v_inst_349_);
v___f_370_ = lean_alloc_closure((void*)(l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_go___redArg___lam__3), 11, 10);
lean_closure_set(v___f_370_, 0, v_acc_355_);
lean_closure_set(v___f_370_, 1, v_inst_349_);
lean_closure_set(v___f_370_, 2, v_inst_350_);
lean_closure_set(v___f_370_, 3, v_inst_351_);
lean_closure_set(v___f_370_, 4, v_inst_352_);
lean_closure_set(v___f_370_, 5, v_inst_353_);
lean_closure_set(v___f_370_, 6, v_p_369_);
lean_closure_set(v___f_370_, 7, v_k_367_);
lean_closure_set(v___f_370_, 8, v_v_368_);
lean_closure_set(v___f_370_, 9, v_toBind_366_);
v___x_371_ = l_Lean_Meta_Grind_Arith_CommRing_getAddFn___redArg(v_inst_351_, v_inst_350_, v_inst_349_, v_inst_352_, v_inst_353_);
v___x_372_ = lean_apply_4(v_toBind_366_, lean_box(0), lean_box(0), v___x_371_, v___f_370_);
return v___x_372_;
}
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_go___redArg___lam__2(lean_object* v_____do__lift_373_, lean_object* v_acc_374_, lean_object* v_inst_375_, lean_object* v_inst_376_, lean_object* v_inst_377_, lean_object* v_inst_378_, lean_object* v_inst_379_, lean_object* v_p_380_, lean_object* v_____do__lift_381_){
_start:
{
lean_object* v___x_382_; lean_object* v___x_383_; 
v___x_382_ = l_Lean_mkAppB(v_____do__lift_373_, v_acc_374_, v_____do__lift_381_);
v___x_383_ = l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_go___redArg(v_inst_375_, v_inst_376_, v_inst_377_, v_inst_378_, v_inst_379_, v_p_380_, v___x_382_);
return v___x_383_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_go(lean_object* v_M_384_, lean_object* v_inst_385_, lean_object* v_inst_386_, lean_object* v_inst_387_, lean_object* v_inst_388_, lean_object* v_inst_389_, lean_object* v_p_390_, lean_object* v_acc_391_){
_start:
{
lean_object* v___x_392_; 
v___x_392_ = l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_go___redArg(v_inst_385_, v_inst_386_, v_inst_387_, v_inst_388_, v_inst_389_, v_p_390_, v_acc_391_);
return v___x_392_;
}
}
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Poly_denoteExpr___redArg___lam__0(lean_object* v_inst_393_, lean_object* v_inst_394_, lean_object* v_inst_395_, lean_object* v_inst_396_, lean_object* v_inst_397_, lean_object* v_p_398_, lean_object* v_____do__lift_399_){
_start:
{
lean_object* v___x_400_; 
v___x_400_ = l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_go___redArg(v_inst_393_, v_inst_394_, v_inst_395_, v_inst_396_, v_inst_397_, v_p_398_, v_____do__lift_399_);
return v___x_400_;
}
}
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Poly_denoteExpr___redArg(lean_object* v_inst_401_, lean_object* v_inst_402_, lean_object* v_inst_403_, lean_object* v_inst_404_, lean_object* v_inst_405_, lean_object* v_p_406_){
_start:
{
if (lean_obj_tag(v_p_406_) == 0)
{
lean_object* v_k_407_; lean_object* v___x_408_; 
v_k_407_ = lean_ctor_get(v_p_406_, 0);
lean_inc(v_k_407_);
lean_dec_ref(v_p_406_);
v___x_408_ = l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg(v_inst_401_, v_inst_402_, v_inst_403_, v_inst_404_, v_inst_405_, v_k_407_);
return v___x_408_;
}
else
{
lean_object* v_toBind_409_; lean_object* v_k_410_; lean_object* v_v_411_; lean_object* v_p_412_; lean_object* v___f_413_; lean_object* v___x_414_; lean_object* v___x_415_; 
v_toBind_409_ = lean_ctor_get(v_inst_401_, 1);
lean_inc(v_toBind_409_);
v_k_410_ = lean_ctor_get(v_p_406_, 0);
lean_inc(v_k_410_);
v_v_411_ = lean_ctor_get(v_p_406_, 1);
lean_inc(v_v_411_);
v_p_412_ = lean_ctor_get(v_p_406_, 2);
lean_inc_ref(v_p_412_);
lean_dec_ref(v_p_406_);
lean_inc_ref(v_inst_405_);
lean_inc_ref(v_inst_404_);
lean_inc(v_inst_403_);
lean_inc_ref(v_inst_402_);
lean_inc_ref(v_inst_401_);
v___f_413_ = lean_alloc_closure((void*)(l_Lean_Grind_CommRing_Poly_denoteExpr___redArg___lam__0), 7, 6);
lean_closure_set(v___f_413_, 0, v_inst_401_);
lean_closure_set(v___f_413_, 1, v_inst_402_);
lean_closure_set(v___f_413_, 2, v_inst_403_);
lean_closure_set(v___f_413_, 3, v_inst_404_);
lean_closure_set(v___f_413_, 4, v_inst_405_);
lean_closure_set(v___f_413_, 5, v_p_412_);
v___x_414_ = l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Grind_CommRing_Poly_denoteExpr_denoteTerm___redArg(v_inst_401_, v_inst_402_, v_inst_403_, v_inst_404_, v_inst_405_, v_k_410_, v_v_411_);
v___x_415_ = lean_apply_4(v_toBind_409_, lean_box(0), lean_box(0), v___x_414_, v___f_413_);
return v___x_415_;
}
}
}
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Poly_denoteExpr(lean_object* v_M_416_, lean_object* v_inst_417_, lean_object* v_inst_418_, lean_object* v_inst_419_, lean_object* v_inst_420_, lean_object* v_inst_421_, lean_object* v_p_422_){
_start:
{
lean_object* v___x_423_; 
v___x_423_ = l_Lean_Grind_CommRing_Poly_denoteExpr___redArg(v_inst_417_, v_inst_418_, v_inst_419_, v_inst_420_, v_inst_421_, v_p_422_);
return v___x_423_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__0(lean_object* v_k_424_, lean_object* v_toPure_425_, lean_object* v_____do__lift_426_){
_start:
{
lean_object* v___x_427_; lean_object* v___x_428_; lean_object* v___x_429_; 
v___x_427_ = l_Lean_mkNatLit(v_k_424_);
v___x_428_ = l_Lean_Expr_app___override(v_____do__lift_426_, v___x_427_);
v___x_429_ = lean_apply_2(v_toPure_425_, lean_box(0), v___x_428_);
return v___x_429_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__1(lean_object* v_k_430_, lean_object* v_toPure_431_, lean_object* v_____do__lift_432_){
_start:
{
lean_object* v___x_433_; lean_object* v___x_434_; lean_object* v___x_435_; 
v___x_433_ = l_Lean_mkIntLit(v_k_430_);
v___x_434_ = l_Lean_Expr_app___override(v_____do__lift_432_, v___x_433_);
v___x_435_ = lean_apply_2(v_toPure_431_, lean_box(0), v___x_434_);
return v___x_435_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__1___boxed(lean_object* v_k_436_, lean_object* v_toPure_437_, lean_object* v_____do__lift_438_){
_start:
{
lean_object* v_res_439_; 
v_res_439_ = l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__1(v_k_436_, v_toPure_437_, v_____do__lift_438_);
lean_dec(v_k_436_);
return v_res_439_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__2(lean_object* v_____do__lift_440_, lean_object* v_toPure_441_, lean_object* v_____do__lift_442_){
_start:
{
lean_object* v___x_443_; lean_object* v___x_444_; 
v___x_443_ = l_Lean_Expr_app___override(v_____do__lift_440_, v_____do__lift_442_);
v___x_444_ = lean_apply_2(v_toPure_441_, lean_box(0), v___x_443_);
return v___x_444_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__13(lean_object* v_k_445_, lean_object* v_____do__lift_446_, lean_object* v_toPure_447_, lean_object* v_____do__lift_448_){
_start:
{
lean_object* v___x_449_; lean_object* v___x_450_; lean_object* v___x_451_; 
v___x_449_ = l_Lean_mkNatLit(v_k_445_);
v___x_450_ = l_Lean_mkAppB(v_____do__lift_446_, v_____do__lift_448_, v___x_449_);
v___x_451_ = lean_apply_2(v_toPure_447_, lean_box(0), v___x_450_);
return v___x_451_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__4(lean_object* v_____do__lift_452_, lean_object* v_____do__lift_453_, lean_object* v_toPure_454_, lean_object* v_____do__lift_455_){
_start:
{
lean_object* v___x_456_; lean_object* v___x_457_; 
v___x_456_ = l_Lean_mkAppB(v_____do__lift_452_, v_____do__lift_453_, v_____do__lift_455_);
v___x_457_ = lean_apply_2(v_toPure_454_, lean_box(0), v___x_456_);
return v___x_457_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__5(lean_object* v_____do__lift_458_, lean_object* v_toPure_459_, lean_object* v_inst_460_, lean_object* v_inst_461_, lean_object* v_inst_462_, lean_object* v_inst_463_, lean_object* v_inst_464_, lean_object* v_getVar_465_, lean_object* v_b_466_, lean_object* v_toBind_467_, lean_object* v_____do__lift_468_){
_start:
{
lean_object* v___f_469_; lean_object* v___x_470_; lean_object* v___x_471_; 
v___f_469_ = lean_alloc_closure((void*)(l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__4), 4, 3);
lean_closure_set(v___f_469_, 0, v_____do__lift_458_);
lean_closure_set(v___f_469_, 1, v_____do__lift_468_);
lean_closure_set(v___f_469_, 2, v_toPure_459_);
v___x_470_ = l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg(v_inst_460_, v_inst_461_, v_inst_462_, v_inst_463_, v_inst_464_, v_getVar_465_, v_b_466_);
v___x_471_ = lean_apply_4(v_toBind_467_, lean_box(0), lean_box(0), v___x_470_, v___f_469_);
return v___x_471_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__6(lean_object* v_toPure_472_, lean_object* v_inst_473_, lean_object* v_inst_474_, lean_object* v_inst_475_, lean_object* v_inst_476_, lean_object* v_inst_477_, lean_object* v_getVar_478_, lean_object* v_b_479_, lean_object* v_toBind_480_, lean_object* v_a_481_, lean_object* v_____do__lift_482_){
_start:
{
lean_object* v___f_483_; lean_object* v___x_484_; lean_object* v___x_485_; 
lean_inc(v_toBind_480_);
lean_inc_ref(v_getVar_478_);
lean_inc_ref(v_inst_477_);
lean_inc_ref(v_inst_476_);
lean_inc(v_inst_475_);
lean_inc_ref(v_inst_474_);
lean_inc_ref(v_inst_473_);
v___f_483_ = lean_alloc_closure((void*)(l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__5), 11, 10);
lean_closure_set(v___f_483_, 0, v_____do__lift_482_);
lean_closure_set(v___f_483_, 1, v_toPure_472_);
lean_closure_set(v___f_483_, 2, v_inst_473_);
lean_closure_set(v___f_483_, 3, v_inst_474_);
lean_closure_set(v___f_483_, 4, v_inst_475_);
lean_closure_set(v___f_483_, 5, v_inst_476_);
lean_closure_set(v___f_483_, 6, v_inst_477_);
lean_closure_set(v___f_483_, 7, v_getVar_478_);
lean_closure_set(v___f_483_, 8, v_b_479_);
lean_closure_set(v___f_483_, 9, v_toBind_480_);
v___x_484_ = l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg(v_inst_473_, v_inst_474_, v_inst_475_, v_inst_476_, v_inst_477_, v_getVar_478_, v_a_481_);
v___x_485_ = lean_apply_4(v_toBind_480_, lean_box(0), lean_box(0), v___x_484_, v___f_483_);
return v___x_485_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__7(lean_object* v_k_486_, lean_object* v_toPure_487_, lean_object* v_inst_488_, lean_object* v_inst_489_, lean_object* v_inst_490_, lean_object* v_inst_491_, lean_object* v_inst_492_, lean_object* v_getVar_493_, lean_object* v_a_494_, lean_object* v_toBind_495_, lean_object* v_____do__lift_496_){
_start:
{
lean_object* v___f_497_; lean_object* v___x_498_; lean_object* v___x_499_; 
v___f_497_ = lean_alloc_closure((void*)(l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__13), 4, 3);
lean_closure_set(v___f_497_, 0, v_k_486_);
lean_closure_set(v___f_497_, 1, v_____do__lift_496_);
lean_closure_set(v___f_497_, 2, v_toPure_487_);
v___x_498_ = l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg(v_inst_488_, v_inst_489_, v_inst_490_, v_inst_491_, v_inst_492_, v_getVar_493_, v_a_494_);
v___x_499_ = lean_apply_4(v_toBind_495_, lean_box(0), lean_box(0), v___x_498_, v___f_497_);
return v___x_499_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg(lean_object* v_inst_500_, lean_object* v_inst_501_, lean_object* v_inst_502_, lean_object* v_inst_503_, lean_object* v_inst_504_, lean_object* v_getVar_505_, lean_object* v_a_506_){
_start:
{
switch(lean_obj_tag(v_a_506_))
{
case 0:
{
lean_object* v_k_507_; lean_object* v___x_508_; 
lean_dec_ref(v_getVar_505_);
v_k_507_ = lean_ctor_get(v_a_506_, 0);
lean_inc(v_k_507_);
lean_dec_ref(v_a_506_);
v___x_508_ = l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg(v_inst_500_, v_inst_501_, v_inst_502_, v_inst_503_, v_inst_504_, v_k_507_);
return v___x_508_;
}
case 1:
{
lean_object* v_toApplicative_509_; lean_object* v_toBind_510_; lean_object* v_toPure_511_; lean_object* v_k_512_; lean_object* v___f_513_; lean_object* v___x_514_; lean_object* v___x_515_; 
v_toApplicative_509_ = lean_ctor_get(v_inst_500_, 0);
lean_dec_ref(v_getVar_505_);
lean_dec_ref(v_inst_501_);
v_toBind_510_ = lean_ctor_get(v_inst_500_, 1);
lean_inc(v_toBind_510_);
v_toPure_511_ = lean_ctor_get(v_toApplicative_509_, 1);
v_k_512_ = lean_ctor_get(v_a_506_, 0);
lean_inc(v_k_512_);
lean_dec_ref(v_a_506_);
lean_inc(v_toPure_511_);
v___f_513_ = lean_alloc_closure((void*)(l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__0), 3, 2);
lean_closure_set(v___f_513_, 0, v_k_512_);
lean_closure_set(v___f_513_, 1, v_toPure_511_);
v___x_514_ = l_Lean_Meta_Grind_Arith_CommRing_getNatCastFn___redArg(v_inst_502_, v_inst_500_, v_inst_503_, v_inst_504_);
v___x_515_ = lean_apply_4(v_toBind_510_, lean_box(0), lean_box(0), v___x_514_, v___f_513_);
return v___x_515_;
}
case 2:
{
lean_object* v_toApplicative_516_; lean_object* v_toBind_517_; lean_object* v_toPure_518_; lean_object* v_k_519_; lean_object* v___f_520_; lean_object* v___x_521_; lean_object* v___x_522_; 
v_toApplicative_516_ = lean_ctor_get(v_inst_500_, 0);
lean_dec_ref(v_getVar_505_);
lean_dec_ref(v_inst_501_);
v_toBind_517_ = lean_ctor_get(v_inst_500_, 1);
lean_inc(v_toBind_517_);
v_toPure_518_ = lean_ctor_get(v_toApplicative_516_, 1);
v_k_519_ = lean_ctor_get(v_a_506_, 0);
lean_inc(v_k_519_);
lean_dec_ref(v_a_506_);
lean_inc(v_toPure_518_);
v___f_520_ = lean_alloc_closure((void*)(l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__1___boxed), 3, 2);
lean_closure_set(v___f_520_, 0, v_k_519_);
lean_closure_set(v___f_520_, 1, v_toPure_518_);
v___x_521_ = l_Lean_Meta_Grind_Arith_CommRing_getIntCastFn___redArg(v_inst_502_, v_inst_500_, v_inst_503_, v_inst_504_);
v___x_522_ = lean_apply_4(v_toBind_517_, lean_box(0), lean_box(0), v___x_521_, v___f_520_);
return v___x_522_;
}
case 3:
{
lean_object* v_toApplicative_523_; lean_object* v_toPure_524_; lean_object* v_i_525_; lean_object* v___x_526_; lean_object* v___x_527_; 
v_toApplicative_523_ = lean_ctor_get(v_inst_500_, 0);
lean_inc_ref(v_toApplicative_523_);
lean_dec_ref(v_inst_504_);
lean_dec_ref(v_inst_503_);
lean_dec(v_inst_502_);
lean_dec_ref(v_inst_501_);
lean_dec_ref(v_inst_500_);
v_toPure_524_ = lean_ctor_get(v_toApplicative_523_, 1);
lean_inc(v_toPure_524_);
lean_dec_ref(v_toApplicative_523_);
v_i_525_ = lean_ctor_get(v_a_506_, 0);
lean_inc(v_i_525_);
lean_dec_ref(v_a_506_);
v___x_526_ = lean_apply_1(v_getVar_505_, v_i_525_);
v___x_527_ = lean_apply_2(v_toPure_524_, lean_box(0), v___x_526_);
return v___x_527_;
}
case 4:
{
lean_object* v_toApplicative_528_; lean_object* v_toBind_529_; lean_object* v_toPure_530_; lean_object* v_a_531_; lean_object* v___f_532_; lean_object* v___x_533_; lean_object* v___x_534_; 
v_toApplicative_528_ = lean_ctor_get(v_inst_500_, 0);
v_toBind_529_ = lean_ctor_get(v_inst_500_, 1);
lean_inc(v_toBind_529_);
v_toPure_530_ = lean_ctor_get(v_toApplicative_528_, 1);
v_a_531_ = lean_ctor_get(v_a_506_, 0);
lean_inc_ref(v_a_531_);
lean_dec_ref(v_a_506_);
lean_inc(v_toBind_529_);
lean_inc_ref(v_inst_504_);
lean_inc_ref(v_inst_503_);
lean_inc(v_inst_502_);
lean_inc_ref(v_inst_501_);
lean_inc_ref(v_inst_500_);
lean_inc(v_toPure_530_);
v___f_532_ = lean_alloc_closure((void*)(l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__3), 10, 9);
lean_closure_set(v___f_532_, 0, v_toPure_530_);
lean_closure_set(v___f_532_, 1, v_inst_500_);
lean_closure_set(v___f_532_, 2, v_inst_501_);
lean_closure_set(v___f_532_, 3, v_inst_502_);
lean_closure_set(v___f_532_, 4, v_inst_503_);
lean_closure_set(v___f_532_, 5, v_inst_504_);
lean_closure_set(v___f_532_, 6, v_getVar_505_);
lean_closure_set(v___f_532_, 7, v_a_531_);
lean_closure_set(v___f_532_, 8, v_toBind_529_);
v___x_533_ = l_Lean_Meta_Grind_Arith_CommRing_getNegFn___redArg(v_inst_502_, v_inst_501_, v_inst_500_, v_inst_503_, v_inst_504_);
v___x_534_ = lean_apply_4(v_toBind_529_, lean_box(0), lean_box(0), v___x_533_, v___f_532_);
return v___x_534_;
}
case 5:
{
lean_object* v_toApplicative_535_; lean_object* v_toBind_536_; lean_object* v_toPure_537_; lean_object* v_a_538_; lean_object* v_b_539_; lean_object* v___f_540_; lean_object* v___x_541_; lean_object* v___x_542_; 
v_toApplicative_535_ = lean_ctor_get(v_inst_500_, 0);
v_toBind_536_ = lean_ctor_get(v_inst_500_, 1);
lean_inc(v_toBind_536_);
v_toPure_537_ = lean_ctor_get(v_toApplicative_535_, 1);
v_a_538_ = lean_ctor_get(v_a_506_, 0);
lean_inc_ref(v_a_538_);
v_b_539_ = lean_ctor_get(v_a_506_, 1);
lean_inc_ref(v_b_539_);
lean_dec_ref(v_a_506_);
lean_inc(v_toBind_536_);
lean_inc_ref(v_inst_504_);
lean_inc_ref(v_inst_503_);
lean_inc(v_inst_502_);
lean_inc_ref(v_inst_501_);
lean_inc_ref(v_inst_500_);
lean_inc(v_toPure_537_);
v___f_540_ = lean_alloc_closure((void*)(l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__6), 11, 10);
lean_closure_set(v___f_540_, 0, v_toPure_537_);
lean_closure_set(v___f_540_, 1, v_inst_500_);
lean_closure_set(v___f_540_, 2, v_inst_501_);
lean_closure_set(v___f_540_, 3, v_inst_502_);
lean_closure_set(v___f_540_, 4, v_inst_503_);
lean_closure_set(v___f_540_, 5, v_inst_504_);
lean_closure_set(v___f_540_, 6, v_getVar_505_);
lean_closure_set(v___f_540_, 7, v_b_539_);
lean_closure_set(v___f_540_, 8, v_toBind_536_);
lean_closure_set(v___f_540_, 9, v_a_538_);
v___x_541_ = l_Lean_Meta_Grind_Arith_CommRing_getAddFn___redArg(v_inst_502_, v_inst_501_, v_inst_500_, v_inst_503_, v_inst_504_);
v___x_542_ = lean_apply_4(v_toBind_536_, lean_box(0), lean_box(0), v___x_541_, v___f_540_);
return v___x_542_;
}
case 6:
{
lean_object* v_toApplicative_543_; lean_object* v_toBind_544_; lean_object* v_toPure_545_; lean_object* v_a_546_; lean_object* v_b_547_; lean_object* v___f_548_; lean_object* v___x_549_; lean_object* v___x_550_; 
v_toApplicative_543_ = lean_ctor_get(v_inst_500_, 0);
v_toBind_544_ = lean_ctor_get(v_inst_500_, 1);
lean_inc(v_toBind_544_);
v_toPure_545_ = lean_ctor_get(v_toApplicative_543_, 1);
v_a_546_ = lean_ctor_get(v_a_506_, 0);
lean_inc_ref(v_a_546_);
v_b_547_ = lean_ctor_get(v_a_506_, 1);
lean_inc_ref(v_b_547_);
lean_dec_ref(v_a_506_);
lean_inc(v_toBind_544_);
lean_inc_ref(v_inst_504_);
lean_inc_ref(v_inst_503_);
lean_inc(v_inst_502_);
lean_inc_ref(v_inst_501_);
lean_inc_ref(v_inst_500_);
lean_inc(v_toPure_545_);
v___f_548_ = lean_alloc_closure((void*)(l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__6), 11, 10);
lean_closure_set(v___f_548_, 0, v_toPure_545_);
lean_closure_set(v___f_548_, 1, v_inst_500_);
lean_closure_set(v___f_548_, 2, v_inst_501_);
lean_closure_set(v___f_548_, 3, v_inst_502_);
lean_closure_set(v___f_548_, 4, v_inst_503_);
lean_closure_set(v___f_548_, 5, v_inst_504_);
lean_closure_set(v___f_548_, 6, v_getVar_505_);
lean_closure_set(v___f_548_, 7, v_b_547_);
lean_closure_set(v___f_548_, 8, v_toBind_544_);
lean_closure_set(v___f_548_, 9, v_a_546_);
v___x_549_ = l_Lean_Meta_Grind_Arith_CommRing_getSubFn___redArg(v_inst_502_, v_inst_501_, v_inst_500_, v_inst_503_, v_inst_504_);
v___x_550_ = lean_apply_4(v_toBind_544_, lean_box(0), lean_box(0), v___x_549_, v___f_548_);
return v___x_550_;
}
case 7:
{
lean_object* v_toApplicative_551_; lean_object* v_toBind_552_; lean_object* v_toPure_553_; lean_object* v_a_554_; lean_object* v_b_555_; lean_object* v___f_556_; lean_object* v___x_557_; lean_object* v___x_558_; 
v_toApplicative_551_ = lean_ctor_get(v_inst_500_, 0);
v_toBind_552_ = lean_ctor_get(v_inst_500_, 1);
lean_inc(v_toBind_552_);
v_toPure_553_ = lean_ctor_get(v_toApplicative_551_, 1);
v_a_554_ = lean_ctor_get(v_a_506_, 0);
lean_inc_ref(v_a_554_);
v_b_555_ = lean_ctor_get(v_a_506_, 1);
lean_inc_ref(v_b_555_);
lean_dec_ref(v_a_506_);
lean_inc(v_toBind_552_);
lean_inc_ref(v_inst_504_);
lean_inc_ref(v_inst_503_);
lean_inc(v_inst_502_);
lean_inc_ref(v_inst_501_);
lean_inc_ref(v_inst_500_);
lean_inc(v_toPure_553_);
v___f_556_ = lean_alloc_closure((void*)(l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__6), 11, 10);
lean_closure_set(v___f_556_, 0, v_toPure_553_);
lean_closure_set(v___f_556_, 1, v_inst_500_);
lean_closure_set(v___f_556_, 2, v_inst_501_);
lean_closure_set(v___f_556_, 3, v_inst_502_);
lean_closure_set(v___f_556_, 4, v_inst_503_);
lean_closure_set(v___f_556_, 5, v_inst_504_);
lean_closure_set(v___f_556_, 6, v_getVar_505_);
lean_closure_set(v___f_556_, 7, v_b_555_);
lean_closure_set(v___f_556_, 8, v_toBind_552_);
lean_closure_set(v___f_556_, 9, v_a_554_);
v___x_557_ = l_Lean_Meta_Grind_Arith_CommRing_getMulFn___redArg(v_inst_502_, v_inst_501_, v_inst_500_, v_inst_503_, v_inst_504_);
v___x_558_ = lean_apply_4(v_toBind_552_, lean_box(0), lean_box(0), v___x_557_, v___f_556_);
return v___x_558_;
}
default: 
{
lean_object* v_toApplicative_559_; lean_object* v_toBind_560_; lean_object* v_toPure_561_; lean_object* v_a_562_; lean_object* v_k_563_; lean_object* v___f_564_; lean_object* v___x_565_; lean_object* v___x_566_; 
v_toApplicative_559_ = lean_ctor_get(v_inst_500_, 0);
v_toBind_560_ = lean_ctor_get(v_inst_500_, 1);
lean_inc(v_toBind_560_);
v_toPure_561_ = lean_ctor_get(v_toApplicative_559_, 1);
v_a_562_ = lean_ctor_get(v_a_506_, 0);
lean_inc_ref(v_a_562_);
v_k_563_ = lean_ctor_get(v_a_506_, 1);
lean_inc(v_k_563_);
lean_dec_ref(v_a_506_);
lean_inc(v_toBind_560_);
lean_inc_ref(v_inst_504_);
lean_inc_ref(v_inst_503_);
lean_inc(v_inst_502_);
lean_inc_ref(v_inst_501_);
lean_inc_ref(v_inst_500_);
lean_inc(v_toPure_561_);
v___f_564_ = lean_alloc_closure((void*)(l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__7), 11, 10);
lean_closure_set(v___f_564_, 0, v_k_563_);
lean_closure_set(v___f_564_, 1, v_toPure_561_);
lean_closure_set(v___f_564_, 2, v_inst_500_);
lean_closure_set(v___f_564_, 3, v_inst_501_);
lean_closure_set(v___f_564_, 4, v_inst_502_);
lean_closure_set(v___f_564_, 5, v_inst_503_);
lean_closure_set(v___f_564_, 6, v_inst_504_);
lean_closure_set(v___f_564_, 7, v_getVar_505_);
lean_closure_set(v___f_564_, 8, v_a_562_);
lean_closure_set(v___f_564_, 9, v_toBind_560_);
v___x_565_ = l_Lean_Meta_Grind_Arith_CommRing_getPowFn___redArg(v_inst_502_, v_inst_501_, v_inst_500_, v_inst_503_, v_inst_504_);
v___x_566_ = lean_apply_4(v_toBind_560_, lean_box(0), lean_box(0), v___x_565_, v___f_564_);
return v___x_566_;
}
}
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__3(lean_object* v_toPure_567_, lean_object* v_inst_568_, lean_object* v_inst_569_, lean_object* v_inst_570_, lean_object* v_inst_571_, lean_object* v_inst_572_, lean_object* v_getVar_573_, lean_object* v_a_574_, lean_object* v_toBind_575_, lean_object* v_____do__lift_576_){
_start:
{
lean_object* v___f_577_; lean_object* v___x_578_; lean_object* v___x_579_; 
v___f_577_ = lean_alloc_closure((void*)(l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg___lam__2), 3, 2);
lean_closure_set(v___f_577_, 0, v_____do__lift_576_);
lean_closure_set(v___f_577_, 1, v_toPure_567_);
v___x_578_ = l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg(v_inst_568_, v_inst_569_, v_inst_570_, v_inst_571_, v_inst_572_, v_getVar_573_, v_a_574_);
v___x_579_ = lean_apply_4(v_toBind_575_, lean_box(0), lean_box(0), v___x_578_, v___f_577_);
return v___x_579_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go(lean_object* v_M_580_, lean_object* v_inst_581_, lean_object* v_inst_582_, lean_object* v_inst_583_, lean_object* v_inst_584_, lean_object* v_inst_585_, lean_object* v_getVar_586_, lean_object* v_a_587_){
_start:
{
lean_object* v___x_588_; 
v___x_588_ = l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg(v_inst_581_, v_inst_582_, v_inst_583_, v_inst_584_, v_inst_585_, v_getVar_586_, v_a_587_);
return v___x_588_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore___redArg(lean_object* v_inst_589_, lean_object* v_inst_590_, lean_object* v_inst_591_, lean_object* v_inst_592_, lean_object* v_inst_593_, lean_object* v_getVar_594_, lean_object* v_e_595_){
_start:
{
lean_object* v___x_596_; 
v___x_596_ = l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg(v_inst_589_, v_inst_590_, v_inst_591_, v_inst_592_, v_inst_593_, v_getVar_594_, v_e_595_);
return v___x_596_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore(lean_object* v_M_597_, lean_object* v_inst_598_, lean_object* v_inst_599_, lean_object* v_inst_600_, lean_object* v_inst_601_, lean_object* v_inst_602_, lean_object* v_getVar_603_, lean_object* v_e_604_){
_start:
{
lean_object* v___x_605_; 
v___x_605_ = l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg(v_inst_598_, v_inst_599_, v_inst_600_, v_inst_601_, v_inst_602_, v_getVar_603_, v_e_604_);
return v___x_605_;
}
}
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Expr_denoteExpr___redArg___lam__0(lean_object* v_ring_606_, lean_object* v___x_607_, lean_object* v_x_608_){
_start:
{
lean_object* v_vars_609_; lean_object* v_size_610_; uint8_t v___x_611_; 
v_vars_609_ = lean_ctor_get(v_ring_606_, 14);
lean_inc_ref(v_vars_609_);
lean_dec_ref(v_ring_606_);
v_size_610_ = lean_ctor_get(v_vars_609_, 2);
v___x_611_ = lean_nat_dec_lt(v_x_608_, v_size_610_);
if (v___x_611_ == 0)
{
lean_object* v___x_612_; 
lean_dec_ref(v_vars_609_);
v___x_612_ = l_outOfBounds___redArg(v___x_607_);
return v___x_612_;
}
else
{
lean_object* v___x_613_; 
v___x_613_ = l_Lean_PersistentArray_get_x21___redArg(v___x_607_, v_vars_609_, v_x_608_);
return v___x_613_;
}
}
}
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Expr_denoteExpr___redArg___lam__0___boxed(lean_object* v_ring_614_, lean_object* v___x_615_, lean_object* v_x_616_){
_start:
{
lean_object* v_res_617_; 
v_res_617_ = l_Lean_Grind_CommRing_Expr_denoteExpr___redArg___lam__0(v_ring_614_, v___x_615_, v_x_616_);
lean_dec(v_x_616_);
return v_res_617_;
}
}
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Expr_denoteExpr___redArg___lam__1(lean_object* v___x_618_, lean_object* v_inst_619_, lean_object* v_inst_620_, lean_object* v_inst_621_, lean_object* v_inst_622_, lean_object* v_inst_623_, lean_object* v_e_624_, lean_object* v_ring_625_){
_start:
{
lean_object* v___f_626_; lean_object* v___x_627_; 
v___f_626_ = lean_alloc_closure((void*)(l_Lean_Grind_CommRing_Expr_denoteExpr___redArg___lam__0___boxed), 3, 2);
lean_closure_set(v___f_626_, 0, v_ring_625_);
lean_closure_set(v___f_626_, 1, v___x_618_);
v___x_627_ = l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg(v_inst_619_, v_inst_620_, v_inst_621_, v_inst_622_, v_inst_623_, v___f_626_, v_e_624_);
return v___x_627_;
}
}
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Expr_denoteExpr___redArg(lean_object* v_inst_628_, lean_object* v_inst_629_, lean_object* v_inst_630_, lean_object* v_inst_631_, lean_object* v_inst_632_, lean_object* v_e_633_){
_start:
{
lean_object* v_toBind_634_; lean_object* v_getRing_635_; lean_object* v___x_636_; lean_object* v___f_637_; lean_object* v___x_638_; 
v_toBind_634_ = lean_ctor_get(v_inst_628_, 1);
lean_inc(v_toBind_634_);
v_getRing_635_ = lean_ctor_get(v_inst_632_, 0);
lean_inc(v_getRing_635_);
v___x_636_ = l_Lean_instInhabitedExpr;
v___f_637_ = lean_alloc_closure((void*)(l_Lean_Grind_CommRing_Expr_denoteExpr___redArg___lam__1), 8, 7);
lean_closure_set(v___f_637_, 0, v___x_636_);
lean_closure_set(v___f_637_, 1, v_inst_628_);
lean_closure_set(v___f_637_, 2, v_inst_629_);
lean_closure_set(v___f_637_, 3, v_inst_630_);
lean_closure_set(v___f_637_, 4, v_inst_631_);
lean_closure_set(v___f_637_, 5, v_inst_632_);
lean_closure_set(v___f_637_, 6, v_e_633_);
v___x_638_ = lean_apply_4(v_toBind_634_, lean_box(0), lean_box(0), v_getRing_635_, v___f_637_);
return v___x_638_;
}
}
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Expr_denoteExpr(lean_object* v_M_639_, lean_object* v_inst_640_, lean_object* v_inst_641_, lean_object* v_inst_642_, lean_object* v_inst_643_, lean_object* v_inst_644_, lean_object* v_e_645_){
_start:
{
lean_object* v___x_646_; 
v___x_646_ = l_Lean_Grind_CommRing_Expr_denoteExpr___redArg(v_inst_640_, v_inst_641_, v_inst_642_, v_inst_643_, v_inst_644_, v_e_645_);
return v___x_646_;
}
}
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Expr_denoteExpr_x27___redArg___lam__0(lean_object* v___x_647_, lean_object* v_vars_648_, lean_object* v_x_649_){
_start:
{
lean_object* v___x_650_; 
v___x_650_ = lean_array_get_borrowed(v___x_647_, v_vars_648_, v_x_649_);
lean_inc(v___x_650_);
return v___x_650_;
}
}
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Expr_denoteExpr_x27___redArg___lam__0___boxed(lean_object* v___x_651_, lean_object* v_vars_652_, lean_object* v_x_653_){
_start:
{
lean_object* v_res_654_; 
v_res_654_ = l_Lean_Grind_CommRing_Expr_denoteExpr_x27___redArg___lam__0(v___x_651_, v_vars_652_, v_x_653_);
lean_dec(v_x_653_);
lean_dec_ref(v_vars_652_);
return v_res_654_;
}
}
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Expr_denoteExpr_x27___redArg(lean_object* v_inst_655_, lean_object* v_inst_656_, lean_object* v_inst_657_, lean_object* v_inst_658_, lean_object* v_inst_659_, lean_object* v_vars_660_, lean_object* v_e_661_){
_start:
{
lean_object* v___x_662_; lean_object* v___f_663_; lean_object* v___x_664_; 
v___x_662_ = l_Lean_instInhabitedExpr;
v___f_663_ = lean_alloc_closure((void*)(l_Lean_Grind_CommRing_Expr_denoteExpr_x27___redArg___lam__0___boxed), 3, 2);
lean_closure_set(v___f_663_, 0, v___x_662_);
lean_closure_set(v___f_663_, 1, v_vars_660_);
v___x_664_ = l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_denoteExprCore_go___redArg(v_inst_655_, v_inst_656_, v_inst_657_, v_inst_658_, v_inst_659_, v___f_663_, v_e_661_);
return v___x_664_;
}
}
LEAN_EXPORT lean_object* l_Lean_Grind_CommRing_Expr_denoteExpr_x27(lean_object* v_M_665_, lean_object* v_inst_666_, lean_object* v_inst_667_, lean_object* v_inst_668_, lean_object* v_inst_669_, lean_object* v_inst_670_, lean_object* v_vars_671_, lean_object* v_e_672_){
_start:
{
lean_object* v___x_673_; 
v___x_673_ = l_Lean_Grind_CommRing_Expr_denoteExpr_x27___redArg(v_inst_666_, v_inst_667_, v_inst_668_, v_inst_669_, v_inst_670_, v_vars_671_, v_e_672_);
return v___x_673_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_mkEq___redArg___lam__0(lean_object* v_a_677_, lean_object* v_b_678_, lean_object* v_toPure_679_, lean_object* v_r_680_){
_start:
{
lean_object* v_type_681_; lean_object* v_u_682_; lean_object* v___x_683_; lean_object* v___x_684_; lean_object* v___x_685_; lean_object* v___x_686_; lean_object* v___x_687_; lean_object* v___x_688_; lean_object* v___x_689_; 
v_type_681_ = lean_ctor_get(v_r_680_, 1);
lean_inc_ref(v_type_681_);
v_u_682_ = lean_ctor_get(v_r_680_, 2);
lean_inc(v_u_682_);
lean_dec_ref(v_r_680_);
v___x_683_ = ((lean_object*)(l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_mkEq___redArg___lam__0___closed__1));
v___x_684_ = l_Lean_Level_succ___override(v_u_682_);
v___x_685_ = lean_box(0);
v___x_686_ = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(v___x_686_, 0, v___x_684_);
lean_ctor_set(v___x_686_, 1, v___x_685_);
v___x_687_ = l_Lean_mkConst(v___x_683_, v___x_686_);
v___x_688_ = l_Lean_mkApp3(v___x_687_, v_type_681_, v_a_677_, v_b_678_);
v___x_689_ = lean_apply_2(v_toPure_679_, lean_box(0), v___x_688_);
return v___x_689_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_mkEq___redArg(lean_object* v_inst_690_, lean_object* v_inst_691_, lean_object* v_a_692_, lean_object* v_b_693_){
_start:
{
lean_object* v_toApplicative_694_; lean_object* v_toBind_695_; lean_object* v_getRing_696_; lean_object* v_toPure_697_; lean_object* v___f_698_; lean_object* v___x_699_; 
v_toApplicative_694_ = lean_ctor_get(v_inst_690_, 0);
lean_inc_ref(v_toApplicative_694_);
v_toBind_695_ = lean_ctor_get(v_inst_690_, 1);
lean_inc(v_toBind_695_);
lean_dec_ref(v_inst_690_);
v_getRing_696_ = lean_ctor_get(v_inst_691_, 0);
lean_inc(v_getRing_696_);
lean_dec_ref(v_inst_691_);
v_toPure_697_ = lean_ctor_get(v_toApplicative_694_, 1);
lean_inc(v_toPure_697_);
lean_dec_ref(v_toApplicative_694_);
v___f_698_ = lean_alloc_closure((void*)(l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_mkEq___redArg___lam__0), 4, 3);
lean_closure_set(v___f_698_, 0, v_a_692_);
lean_closure_set(v___f_698_, 1, v_b_693_);
lean_closure_set(v___f_698_, 2, v_toPure_697_);
v___x_699_ = lean_apply_4(v_toBind_695_, lean_box(0), lean_box(0), v_getRing_696_, v___f_698_);
return v___x_699_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_mkEq(lean_object* v_M_700_, lean_object* v_inst_701_, lean_object* v_inst_702_, lean_object* v_a_703_, lean_object* v_b_704_){
_start:
{
lean_object* v___x_705_; 
v___x_705_ = l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_mkEq___redArg(v_inst_701_, v_inst_702_, v_a_703_, v_b_704_);
return v___x_705_;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_EqCnstr_denoteExpr___redArg___lam__0(lean_object* v_inst_706_, lean_object* v_inst_707_, lean_object* v_____do__lift_708_, lean_object* v_____do__lift_709_){
_start:
{
lean_object* v___x_710_; 
v___x_710_ = l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_mkEq___redArg(v_inst_706_, v_inst_707_, v_____do__lift_708_, v_____do__lift_709_);
return v___x_710_;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_EqCnstr_denoteExpr___redArg___lam__1(lean_object* v_inst_711_, lean_object* v_inst_712_, lean_object* v_inst_713_, lean_object* v_inst_714_, lean_object* v_inst_715_, lean_object* v_toBind_716_, lean_object* v_____do__lift_717_){
_start:
{
lean_object* v___f_718_; lean_object* v___x_719_; lean_object* v___x_720_; lean_object* v___x_721_; 
lean_inc_ref(v_inst_712_);
lean_inc_ref(v_inst_711_);
v___f_718_ = lean_alloc_closure((void*)(l_Lean_Meta_Grind_Arith_CommRing_EqCnstr_denoteExpr___redArg___lam__0), 4, 3);
lean_closure_set(v___f_718_, 0, v_inst_711_);
lean_closure_set(v___f_718_, 1, v_inst_712_);
lean_closure_set(v___f_718_, 2, v_____do__lift_717_);
v___x_719_ = lean_obj_once(&l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__1___closed__1, &l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__1___closed__1_once, _init_l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__1___closed__1);
v___x_720_ = l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg(v_inst_711_, v_inst_713_, v_inst_714_, v_inst_715_, v_inst_712_, v___x_719_);
v___x_721_ = lean_apply_4(v_toBind_716_, lean_box(0), lean_box(0), v___x_720_, v___f_718_);
return v___x_721_;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_EqCnstr_denoteExpr___redArg(lean_object* v_inst_722_, lean_object* v_inst_723_, lean_object* v_inst_724_, lean_object* v_inst_725_, lean_object* v_inst_726_, lean_object* v_c_727_){
_start:
{
lean_object* v_toBind_728_; lean_object* v_p_729_; lean_object* v___f_730_; lean_object* v___x_731_; lean_object* v___x_732_; 
v_toBind_728_ = lean_ctor_get(v_inst_722_, 1);
lean_inc(v_toBind_728_);
v_p_729_ = lean_ctor_get(v_c_727_, 0);
lean_inc_ref(v_p_729_);
lean_dec_ref(v_c_727_);
lean_inc(v_toBind_728_);
lean_inc_ref(v_inst_725_);
lean_inc(v_inst_724_);
lean_inc_ref(v_inst_723_);
lean_inc_ref(v_inst_726_);
lean_inc_ref(v_inst_722_);
v___f_730_ = lean_alloc_closure((void*)(l_Lean_Meta_Grind_Arith_CommRing_EqCnstr_denoteExpr___redArg___lam__1), 7, 6);
lean_closure_set(v___f_730_, 0, v_inst_722_);
lean_closure_set(v___f_730_, 1, v_inst_726_);
lean_closure_set(v___f_730_, 2, v_inst_723_);
lean_closure_set(v___f_730_, 3, v_inst_724_);
lean_closure_set(v___f_730_, 4, v_inst_725_);
lean_closure_set(v___f_730_, 5, v_toBind_728_);
v___x_731_ = l_Lean_Grind_CommRing_Poly_denoteExpr___redArg(v_inst_722_, v_inst_723_, v_inst_724_, v_inst_725_, v_inst_726_, v_p_729_);
v___x_732_ = lean_apply_4(v_toBind_728_, lean_box(0), lean_box(0), v___x_731_, v___f_730_);
return v___x_732_;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_EqCnstr_denoteExpr(lean_object* v_M_733_, lean_object* v_inst_734_, lean_object* v_inst_735_, lean_object* v_inst_736_, lean_object* v_inst_737_, lean_object* v_inst_738_, lean_object* v_c_739_){
_start:
{
lean_object* v___x_740_; 
v___x_740_ = l_Lean_Meta_Grind_Arith_CommRing_EqCnstr_denoteExpr___redArg(v_inst_734_, v_inst_735_, v_inst_736_, v_inst_737_, v_inst_738_, v_c_739_);
return v___x_740_;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_PolyDerivation_denoteExpr___redArg(lean_object* v_inst_741_, lean_object* v_inst_742_, lean_object* v_inst_743_, lean_object* v_inst_744_, lean_object* v_inst_745_, lean_object* v_d_746_){
_start:
{
lean_object* v___x_747_; lean_object* v___x_748_; 
v___x_747_ = l_Lean_Meta_Grind_Arith_CommRing_PolyDerivation_p(v_d_746_);
v___x_748_ = l_Lean_Grind_CommRing_Poly_denoteExpr___redArg(v_inst_741_, v_inst_742_, v_inst_743_, v_inst_744_, v_inst_745_, v___x_747_);
return v___x_748_;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_PolyDerivation_denoteExpr___redArg___boxed(lean_object* v_inst_749_, lean_object* v_inst_750_, lean_object* v_inst_751_, lean_object* v_inst_752_, lean_object* v_inst_753_, lean_object* v_d_754_){
_start:
{
lean_object* v_res_755_; 
v_res_755_ = l_Lean_Meta_Grind_Arith_CommRing_PolyDerivation_denoteExpr___redArg(v_inst_749_, v_inst_750_, v_inst_751_, v_inst_752_, v_inst_753_, v_d_754_);
lean_dec_ref(v_d_754_);
return v_res_755_;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_PolyDerivation_denoteExpr(lean_object* v_M_756_, lean_object* v_inst_757_, lean_object* v_inst_758_, lean_object* v_inst_759_, lean_object* v_inst_760_, lean_object* v_inst_761_, lean_object* v_d_762_){
_start:
{
lean_object* v___x_763_; 
v___x_763_ = l_Lean_Meta_Grind_Arith_CommRing_PolyDerivation_denoteExpr___redArg(v_inst_757_, v_inst_758_, v_inst_759_, v_inst_760_, v_inst_761_, v_d_762_);
return v___x_763_;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_PolyDerivation_denoteExpr___boxed(lean_object* v_M_764_, lean_object* v_inst_765_, lean_object* v_inst_766_, lean_object* v_inst_767_, lean_object* v_inst_768_, lean_object* v_inst_769_, lean_object* v_d_770_){
_start:
{
lean_object* v_res_771_; 
v_res_771_ = l_Lean_Meta_Grind_Arith_CommRing_PolyDerivation_denoteExpr(v_M_764_, v_inst_765_, v_inst_766_, v_inst_767_, v_inst_768_, v_inst_769_, v_d_770_);
lean_dec_ref(v_d_770_);
return v_res_771_;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_DiseqCnstr_denoteExpr___redArg___lam__0(lean_object* v_toPure_772_, lean_object* v_____do__lift_773_){
_start:
{
lean_object* v___x_774_; lean_object* v___x_775_; 
v___x_774_ = l_Lean_mkNot(v_____do__lift_773_);
v___x_775_ = lean_apply_2(v_toPure_772_, lean_box(0), v___x_774_);
return v___x_775_;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_DiseqCnstr_denoteExpr___redArg___lam__1(lean_object* v_inst_776_, lean_object* v_inst_777_, lean_object* v_____do__lift_778_, lean_object* v_toBind_779_, lean_object* v___f_780_, lean_object* v_____do__lift_781_){
_start:
{
lean_object* v___x_782_; lean_object* v___x_783_; 
v___x_782_ = l___private_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr_0__Lean_Meta_Grind_Arith_CommRing_mkEq___redArg(v_inst_776_, v_inst_777_, v_____do__lift_778_, v_____do__lift_781_);
v___x_783_ = lean_apply_4(v_toBind_779_, lean_box(0), lean_box(0), v___x_782_, v___f_780_);
return v___x_783_;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_DiseqCnstr_denoteExpr___redArg___lam__2(lean_object* v_inst_784_, lean_object* v_inst_785_, lean_object* v_toBind_786_, lean_object* v___f_787_, lean_object* v_inst_788_, lean_object* v_inst_789_, lean_object* v_inst_790_, lean_object* v_____do__lift_791_){
_start:
{
lean_object* v___f_792_; lean_object* v___x_793_; lean_object* v___x_794_; lean_object* v___x_795_; 
lean_inc(v_toBind_786_);
lean_inc_ref(v_inst_785_);
lean_inc_ref(v_inst_784_);
v___f_792_ = lean_alloc_closure((void*)(l_Lean_Meta_Grind_Arith_CommRing_DiseqCnstr_denoteExpr___redArg___lam__1), 6, 5);
lean_closure_set(v___f_792_, 0, v_inst_784_);
lean_closure_set(v___f_792_, 1, v_inst_785_);
lean_closure_set(v___f_792_, 2, v_____do__lift_791_);
lean_closure_set(v___f_792_, 3, v_toBind_786_);
lean_closure_set(v___f_792_, 4, v___f_787_);
v___x_793_ = lean_obj_once(&l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__1___closed__1, &l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__1___closed__1_once, _init_l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg___lam__1___closed__1);
v___x_794_ = l_Lean_Meta_Grind_Arith_CommRing_denoteNum___redArg(v_inst_784_, v_inst_788_, v_inst_789_, v_inst_790_, v_inst_785_, v___x_793_);
v___x_795_ = lean_apply_4(v_toBind_786_, lean_box(0), lean_box(0), v___x_794_, v___f_792_);
return v___x_795_;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_DiseqCnstr_denoteExpr___redArg(lean_object* v_inst_796_, lean_object* v_inst_797_, lean_object* v_inst_798_, lean_object* v_inst_799_, lean_object* v_inst_800_, lean_object* v_c_801_){
_start:
{
lean_object* v_toApplicative_802_; lean_object* v_toBind_803_; lean_object* v_d_804_; lean_object* v_toPure_805_; lean_object* v___x_806_; lean_object* v___f_807_; lean_object* v___f_808_; lean_object* v___x_809_; 
v_toApplicative_802_ = lean_ctor_get(v_inst_796_, 0);
v_toBind_803_ = lean_ctor_get(v_inst_796_, 1);
lean_inc(v_toBind_803_);
v_d_804_ = lean_ctor_get(v_c_801_, 4);
v_toPure_805_ = lean_ctor_get(v_toApplicative_802_, 1);
lean_inc_ref(v_inst_800_);
lean_inc_ref(v_inst_799_);
lean_inc(v_inst_798_);
lean_inc_ref(v_inst_797_);
lean_inc_ref(v_inst_796_);
v___x_806_ = l_Lean_Meta_Grind_Arith_CommRing_PolyDerivation_denoteExpr___redArg(v_inst_796_, v_inst_797_, v_inst_798_, v_inst_799_, v_inst_800_, v_d_804_);
lean_inc(v_toPure_805_);
v___f_807_ = lean_alloc_closure((void*)(l_Lean_Meta_Grind_Arith_CommRing_DiseqCnstr_denoteExpr___redArg___lam__0), 2, 1);
lean_closure_set(v___f_807_, 0, v_toPure_805_);
lean_inc(v_toBind_803_);
v___f_808_ = lean_alloc_closure((void*)(l_Lean_Meta_Grind_Arith_CommRing_DiseqCnstr_denoteExpr___redArg___lam__2), 8, 7);
lean_closure_set(v___f_808_, 0, v_inst_796_);
lean_closure_set(v___f_808_, 1, v_inst_800_);
lean_closure_set(v___f_808_, 2, v_toBind_803_);
lean_closure_set(v___f_808_, 3, v___f_807_);
lean_closure_set(v___f_808_, 4, v_inst_797_);
lean_closure_set(v___f_808_, 5, v_inst_798_);
lean_closure_set(v___f_808_, 6, v_inst_799_);
v___x_809_ = lean_apply_4(v_toBind_803_, lean_box(0), lean_box(0), v___x_806_, v___f_808_);
return v___x_809_;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_DiseqCnstr_denoteExpr___redArg___boxed(lean_object* v_inst_810_, lean_object* v_inst_811_, lean_object* v_inst_812_, lean_object* v_inst_813_, lean_object* v_inst_814_, lean_object* v_c_815_){
_start:
{
lean_object* v_res_816_; 
v_res_816_ = l_Lean_Meta_Grind_Arith_CommRing_DiseqCnstr_denoteExpr___redArg(v_inst_810_, v_inst_811_, v_inst_812_, v_inst_813_, v_inst_814_, v_c_815_);
lean_dec_ref(v_c_815_);
return v_res_816_;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_DiseqCnstr_denoteExpr(lean_object* v_M_817_, lean_object* v_inst_818_, lean_object* v_inst_819_, lean_object* v_inst_820_, lean_object* v_inst_821_, lean_object* v_inst_822_, lean_object* v_c_823_){
_start:
{
lean_object* v___x_824_; 
v___x_824_ = l_Lean_Meta_Grind_Arith_CommRing_DiseqCnstr_denoteExpr___redArg(v_inst_818_, v_inst_819_, v_inst_820_, v_inst_821_, v_inst_822_, v_c_823_);
return v___x_824_;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Arith_CommRing_DiseqCnstr_denoteExpr___boxed(lean_object* v_M_825_, lean_object* v_inst_826_, lean_object* v_inst_827_, lean_object* v_inst_828_, lean_object* v_inst_829_, lean_object* v_inst_830_, lean_object* v_c_831_){
_start:
{
lean_object* v_res_832_; 
v_res_832_ = l_Lean_Meta_Grind_Arith_CommRing_DiseqCnstr_denoteExpr(v_M_825_, v_inst_826_, v_inst_827_, v_inst_828_, v_inst_829_, v_inst_830_, v_c_831_);
lean_dec_ref(v_c_831_);
return v_res_832_;
}
}
lean_object* runtime_initialize_Lean_Meta_Tactic_Grind_Arith_CommRing_Functions(uint8_t builtin);
static bool _G_runtime_initialized = false;
LEAN_EXPORT lean_object* runtime_initialize_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr(uint8_t builtin) {
lean_object * res;
if (_G_runtime_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_runtime_initialized = true;
res = runtime_initialize_Lean_Meta_Tactic_Grind_Arith_CommRing_Functions(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
static bool _G_meta_initialized = false;
LEAN_EXPORT lean_object* meta_initialize_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr(uint8_t builtin) {
lean_object * res;
if (_G_meta_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_meta_initialized = true;
return lean_io_result_mk_ok(lean_box(0));
}
lean_object* initialize_Lean_Meta_Tactic_Grind_Arith_CommRing_Functions(uint8_t builtin);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr(uint8_t builtin) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Lean_Meta_Tactic_Grind_Arith_CommRing_Functions(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = meta_initialize_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return initialize_Lean_Meta_Tactic_Grind_Arith_CommRing_DenoteExpr(builtin);
}
#ifdef __cplusplus
}
#endif
