60 lines
3.1 KiB
C++
60 lines
3.1 KiB
C++
/*
|
|
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
*/
|
|
// Automatically generated file, DO NOT EDIT
|
|
#include "kernel/environment.h"
|
|
#include "kernel/decl_macros.h"
|
|
namespace lean {
|
|
MK_CONSTANT(Nat, name("Nat"));
|
|
MK_CONSTANT(Nat_ge_fn, name({"Nat", "ge"}));
|
|
MK_CONSTANT(Nat_lt_fn, name({"Nat", "lt"}));
|
|
MK_CONSTANT(Nat_gt_fn, name({"Nat", "gt"}));
|
|
MK_CONSTANT(Nat_id_fn, name({"Nat", "id"}));
|
|
MK_CONSTANT(Nat_succ_nz_fn, name({"Nat", "succ_nz"}));
|
|
MK_CONSTANT(Nat_succ_inj_fn, name({"Nat", "succ_inj"}));
|
|
MK_CONSTANT(Nat_add_zeror_fn, name({"Nat", "add_zeror"}));
|
|
MK_CONSTANT(Nat_add_succr_fn, name({"Nat", "add_succr"}));
|
|
MK_CONSTANT(Nat_mul_zeror_fn, name({"Nat", "mul_zeror"}));
|
|
MK_CONSTANT(Nat_mul_succr_fn, name({"Nat", "mul_succr"}));
|
|
MK_CONSTANT(Nat_le_def_fn, name({"Nat", "le_def"}));
|
|
MK_CONSTANT(Nat_induction_fn, name({"Nat", "induction"}));
|
|
MK_CONSTANT(Nat_induction_on_fn, name({"Nat", "induction_on"}));
|
|
MK_CONSTANT(Nat_pred_nz_fn, name({"Nat", "pred_nz"}));
|
|
MK_CONSTANT(Nat_discriminate_fn, name({"Nat", "discriminate"}));
|
|
MK_CONSTANT(Nat_add_zerol_fn, name({"Nat", "add_zerol"}));
|
|
MK_CONSTANT(Nat_add_succl_fn, name({"Nat", "add_succl"}));
|
|
MK_CONSTANT(Nat_add_comm_fn, name({"Nat", "add_comm"}));
|
|
MK_CONSTANT(Nat_add_assoc_fn, name({"Nat", "add_assoc"}));
|
|
MK_CONSTANT(Nat_mul_zerol_fn, name({"Nat", "mul_zerol"}));
|
|
MK_CONSTANT(Nat_mul_succl_fn, name({"Nat", "mul_succl"}));
|
|
MK_CONSTANT(Nat_mul_onel_fn, name({"Nat", "mul_onel"}));
|
|
MK_CONSTANT(Nat_mul_oner_fn, name({"Nat", "mul_oner"}));
|
|
MK_CONSTANT(Nat_mul_comm_fn, name({"Nat", "mul_comm"}));
|
|
MK_CONSTANT(Nat_distributer_fn, name({"Nat", "distributer"}));
|
|
MK_CONSTANT(Nat_distributel_fn, name({"Nat", "distributel"}));
|
|
MK_CONSTANT(Nat_mul_assoc_fn, name({"Nat", "mul_assoc"}));
|
|
MK_CONSTANT(Nat_add_left_comm_fn, name({"Nat", "add_left_comm"}));
|
|
MK_CONSTANT(Nat_mul_left_comm_fn, name({"Nat", "mul_left_comm"}));
|
|
MK_CONSTANT(Nat_add_injr_fn, name({"Nat", "add_injr"}));
|
|
MK_CONSTANT(Nat_add_injl_fn, name({"Nat", "add_injl"}));
|
|
MK_CONSTANT(Nat_add_eqz_fn, name({"Nat", "add_eqz"}));
|
|
MK_CONSTANT(Nat_le_intro_fn, name({"Nat", "le_intro"}));
|
|
MK_CONSTANT(Nat_le_elim_fn, name({"Nat", "le_elim"}));
|
|
MK_CONSTANT(Nat_le_refl_fn, name({"Nat", "le_refl"}));
|
|
MK_CONSTANT(Nat_le_zero_fn, name({"Nat", "le_zero"}));
|
|
MK_CONSTANT(Nat_le_trans_fn, name({"Nat", "le_trans"}));
|
|
MK_CONSTANT(Nat_le_add_fn, name({"Nat", "le_add"}));
|
|
MK_CONSTANT(Nat_le_antisym_fn, name({"Nat", "le_antisym"}));
|
|
MK_CONSTANT(Nat_not_lt_0_fn, name({"Nat", "not_lt_0"}));
|
|
MK_CONSTANT(Nat_lt_intro_fn, name({"Nat", "lt_intro"}));
|
|
MK_CONSTANT(Nat_lt_elim_fn, name({"Nat", "lt_elim"}));
|
|
MK_CONSTANT(Nat_lt_le_fn, name({"Nat", "lt_le"}));
|
|
MK_CONSTANT(Nat_lt_ne_fn, name({"Nat", "lt_ne"}));
|
|
MK_CONSTANT(Nat_lt_nrefl_fn, name({"Nat", "lt_nrefl"}));
|
|
MK_CONSTANT(Nat_lt_trans_fn, name({"Nat", "lt_trans"}));
|
|
MK_CONSTANT(Nat_lt_le_trans_fn, name({"Nat", "lt_le_trans"}));
|
|
MK_CONSTANT(Nat_le_lt_trans_fn, name({"Nat", "le_lt_trans"}));
|
|
MK_CONSTANT(Nat_ne_lt_succ_fn, name({"Nat", "ne_lt_succ"}));
|
|
MK_CONSTANT(Nat_strong_induction_fn, name({"Nat", "strong_induction"}));
|
|
}
|