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

chore: update stage0

Browse source
This commit is contained in:
Lean stage0 autoupdater 2026-03-07 00:02:16 +00:00
parent c1bcc4d1ac
commit c948d24b6d
28 changed files with 17869 additions and 7431 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
stage0/src/kernel/environment.cpp generated
View file

@ -197,9 +197,9 @@ environment environment::add_theorem(declaration const & d, bool check) const {
sharecommon_persistent_fn share;
expr val(share(v.get_value().raw()));
expr type(share(v.get_type().raw()));
check_constant_val(*this, v.to_constant_val(), checker);
if (!checker.is_prop(type))
throw theorem_type_is_not_prop(*this, v.get_name(), type);
check_constant_val(*this, v.to_constant_val(), checker);
check_no_metavar_no_fvar(*this, v.get_name(), val);
expr val_type = checker.check(val, v.get_lparams());
if (!checker.is_def_eq(val_type, type))

30
stage0/src/kernel/type_checker.cpp generated
View file

@ -483,12 +483,12 @@ expr type_checker::whnf_core(expr const & e, bool cheap_rec, bool cheap_proj) {
}
/** \brief Return some definition \c d iff \c e is a target for delta-reduction, and the given definition is the one
to be expanded. */
to be expanded. If \c is_delta succeeds, then \c unfold_definition will also succeed. */
optional<constant_info> type_checker::is_delta(expr const & e) const {
expr const & f = get_app_fn(e);
if (is_constant(f)) {
if (optional<constant_info> info = env().find(const_name(f)))
if (info->has_value())
if (info->has_value() && length(const_levels(f)) == info->get_num_lparams())
return info;
}
return none_constant_info();
@ -499,20 +499,18 @@ optional<expr> type_checker::unfold_definition_core(expr const & e) {
if (auto d = is_delta(e)) {
levels const & us = const_levels(e);
unsigned len = length(us);
if (len == d->get_num_lparams()) {
if (m_diag) {
m_diag->record_unfold(d->get_name());
}
if (len > 0) {
auto it = m_st->m_unfold.find(e);
if (it != m_st->m_unfold.end())
return some_expr(it->second);
expr result = instantiate_value_lparams(*d, us);
m_st->m_unfold.insert(mk_pair(e, result));
return some_expr(result);
} else {
return some_expr(instantiate_value_lparams(*d, us));
}
if (m_diag) {
m_diag->record_unfold(d->get_name());
}
if (len > 0) {
auto it = m_st->m_unfold.find(e);
if (it != m_st->m_unfold.end())
return some_expr(it->second);
expr result = instantiate_value_lparams(*d, us);
m_st->m_unfold.insert(mk_pair(e, result));
return some_expr(result);
} else {
return some_expr(instantiate_value_lparams(*d, us));
}
}
}

1
stage0/src/runtime/CMakeLists.txt generated
View file

@ -21,7 +21,6 @@ set(
sharecommon.cpp
stack_overflow.cpp
process.cpp
demangle.cpp
object_ref.cpp
mpn.cpp
mutex.cpp

792
stage0/src/runtime/demangle.cpp generated
View file

@ -1,792 +0,0 @@
/*
Copyright (c) 2025 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
C++ port of the Lean name demangling algorithm (Name.demangleAux from
NameMangling.lean) and human-friendly postprocessing. Used to make
runtime backtraces readable.
*/
#include <cstdlib>
#include <cstring>
#include <string>
#include <vector>
#include "runtime/demangle.h"
namespace {
// ---------------------------------------------------------------------------
// Name component: either a string or a number
// ---------------------------------------------------------------------------
struct Component {
bool is_num;
std::string str;
unsigned num;
Component() : is_num(false), num(0) {}
static Component mk_str(std::string s) { Component c; c.str = std::move(s); return c; }
static Component mk_str(char ch) { Component c; c.str = std::string(1, ch); return c; }
static Component mk_num(unsigned n) { Component c; c.is_num = true; c.num = n; return c; }
};
using Components = std::vector<Component>;
// ---------------------------------------------------------------------------
// Hex parsing and UTF-8 encoding
// ---------------------------------------------------------------------------
int parse_hex(const char * s, int pos, int len, int n_digits, unsigned & out_val) {
if (pos + n_digits > len) return 0;
unsigned val = 0;
for (int i = 0; i < n_digits; i++) {
char c = s[pos + i];
if (c >= '0' && c <= '9')
val = (val << 4) | (unsigned)(c - '0');
else if (c >= 'a' && c <= 'f')
val = (val << 4) | (unsigned)(c - 'a' + 10);
else
return 0;
}
out_val = val;
return n_digits;
}
void append_utf8(std::string & out, unsigned cp) {
if (cp < 0x80) {
out += (char)cp;
} else if (cp < 0x800) {
out += (char)(0xC0 | (cp >> 6));
out += (char)(0x80 | (cp & 0x3F));
} else if (cp < 0x10000) {
out += (char)(0xE0 | (cp >> 12));
out += (char)(0x80 | ((cp >> 6) & 0x3F));
out += (char)(0x80 | (cp & 0x3F));
} else if (cp < 0x110000) {
out += (char)(0xF0 | (cp >> 18));
out += (char)(0x80 | ((cp >> 12) & 0x3F));
out += (char)(0x80 | ((cp >> 6) & 0x3F));
out += (char)(0x80 | (cp & 0x3F));
}
}
// ---------------------------------------------------------------------------
// Core demangling: produces a component list
// Port of Name.demangleAux from NameMangling.lean
// ---------------------------------------------------------------------------
void demangle_main(const char * s, int pos, int len,
std::string & acc, int ucount, Components & out);
void name_start(const char * s, int pos, int len, Components & out);
void decode_num(const char * s, int pos, int len,
unsigned n, Components & out) {
while (pos < len) {
char ch = s[pos];
if (ch >= '0' && ch <= '9') {
n = n * 10 + (unsigned)(ch - '0');
pos++;
} else {
pos++; // skip trailing '_'
out.push_back(Component::mk_num(n));
if (pos >= len) return;
pos++; // skip separator '_'
name_start(s, pos, len, out);
return;
}
}
out.push_back(Component::mk_num(n));
}
void name_start(const char * s, int pos, int len, Components & out) {
if (pos >= len) return;
char ch = s[pos];
pos++;
if (ch >= '0' && ch <= '9') {
if (ch == '0' && pos < len && s[pos] == '0') {
pos++;
std::string acc;
demangle_main(s, pos, len, acc, 0, out);
} else {
decode_num(s, pos, len, (unsigned)(ch - '0'), out);
}
} else if (ch == '_') {
std::string acc;
demangle_main(s, pos, len, acc, 1, out);
} else {
std::string acc(1, ch);
demangle_main(s, pos, len, acc, 0, out);
}
}
void demangle_main(const char * s, int pos, int len,
std::string & acc, int ucount, Components & out) {
while (pos < len) {
char ch = s[pos];
pos++;
if (ch == '_') { ucount++; continue; }
if (ucount % 2 == 0) {
for (int i = 0; i < ucount / 2; i++) acc += '_';
acc += ch;
ucount = 0;
continue;
}
// Odd ucount: separator or escape
if (ch >= '0' && ch <= '9') {
for (int i = 0; i < ucount / 2; i++) acc += '_';
out.push_back(Component::mk_str(std::move(acc)));
if (ch == '0' && pos < len && s[pos] == '0') {
pos++;
acc.clear();
demangle_main(s, pos, len, acc, 0, out);
return;
} else {
decode_num(s, pos, len, (unsigned)(ch - '0'), out);
return;
}
}
unsigned hex_val;
int consumed;
if (ch == 'x') {
consumed = parse_hex(s, pos, len, 2, hex_val);
if (consumed > 0) {
for (int i = 0; i < ucount / 2; i++) acc += '_';
append_utf8(acc, hex_val);
pos += consumed; ucount = 0; continue;
}
}
if (ch == 'u') {
consumed = parse_hex(s, pos, len, 4, hex_val);
if (consumed > 0) {
for (int i = 0; i < ucount / 2; i++) acc += '_';
append_utf8(acc, hex_val);
pos += consumed; ucount = 0; continue;
}
}
if (ch == 'U') {
consumed = parse_hex(s, pos, len, 8, hex_val);
if (consumed > 0) {
for (int i = 0; i < ucount / 2; i++) acc += '_';
append_utf8(acc, hex_val);
pos += consumed; ucount = 0; continue;
}
}
// Name separator
out.push_back(Component::mk_str(std::move(acc)));
acc.clear();
for (int i = 0; i < ucount / 2; i++) acc += '_';
acc += ch;
ucount = 0;
}
for (int i = 0; i < ucount / 2; i++) acc += '_';
if (!acc.empty())
out.push_back(Component::mk_str(std::move(acc)));
}
bool demangle_body(const char * s, int len, Components & out) {
if (len == 0) return false;
name_start(s, 0, len, out);
return !out.empty();
}
// Convenience: demangle to flat dot-separated string (used for lp_ validation)
bool demangle_body_flat(const char * s, int len, std::string & out) {
Components comps;
if (!demangle_body(s, len, comps)) return false;
for (size_t i = 0; i < comps.size(); i++) {
if (i > 0) out += '.';
if (comps[i].is_num) out += std::to_string(comps[i].num);
else out += comps[i].str;
}
return true;
}
// ---------------------------------------------------------------------------
// Format components as dot-separated string
// ---------------------------------------------------------------------------
std::string format_name(const Components & comps) {
std::string out;
for (size_t i = 0; i < comps.size(); i++) {
if (i > 0) out += '.';
if (comps[i].is_num) out += std::to_string(comps[i].num);
else out += comps[i].str;
}
return out;
}
// ---------------------------------------------------------------------------
// Human-friendly postprocessing
// Port of postprocess_name from lean_demangle.py
// ---------------------------------------------------------------------------
// Suffix flag labels (UTF-8 encoded)
static const char * FLAG_ARITY_DOWN = "arity\xe2\x86\x93"; // arity↓
static const char * FLAG_BOXED = "boxed";
static const char * FLAG_IMPL = "impl";
static const char * FLAG_LAMBDA = "\xce\xbb"; // λ
static const char * FLAG_JP = "jp";
static const char * FLAG_CLOSED = "closed";
// Check if a string consists entirely of ASCII digits.
bool is_all_digits(const char * s) {
if (!*s) return false;
while (*s) { if (*s < '0' || *s > '9') return false; s++; }
return true;
}
bool starts_with_str(const std::string & s, const char * prefix) {
size_t plen = strlen(prefix);
return s.size() >= plen && s.compare(0, plen, prefix) == 0;
}
// Match a compiler-generated suffix component. Returns flag label or nullptr.
const char * match_suffix(const Component & c) {
if (c.is_num) return nullptr;
const std::string & s = c.str;
// Exact matches
if (s == "_redArg") return FLAG_ARITY_DOWN;
if (s == "_boxed") return FLAG_BOXED;
if (s == "_impl") return FLAG_IMPL;
// Exact or indexed prefix matches
if (s == "_lam" || s == "_lambda" || s == "_elam") return FLAG_LAMBDA;
if (s == "_jp") return FLAG_JP;
if (s == "_closed") return FLAG_CLOSED;
// Indexed: _lam_N, _lambda_N, _elam_N, _jp_N, _closed_N
struct { const char * prefix; size_t len; const char * flag; } indexed[] = {
{"_lam_", 5, FLAG_LAMBDA},
{"_lambda_", 8, FLAG_LAMBDA},
{"_elam_", 6, FLAG_LAMBDA},
{"_jp_", 4, FLAG_JP},
{"_closed_", 8, FLAG_CLOSED},
};
for (auto & e : indexed) {
if (s.size() > e.len && s.compare(0, e.len, e.prefix) == 0 &&
is_all_digits(s.c_str() + e.len))
return e.flag;
}
return nullptr;
}
// Check if component is a spec_N index.
bool is_spec_index(const Component & c) {
if (c.is_num) return false;
return starts_with_str(c.str, "spec_") && c.str.size() > 5 &&
is_all_digits(c.str.c_str() + 5);
}
// Strip _private.Module.0. prefix. Returns (begin index past the strip, is_private).
struct StripResult { size_t begin; bool is_private; };
StripResult strip_private(const Components & parts, size_t begin, size_t end) {
if (end - begin >= 3 && !parts[begin].is_num && parts[begin].str == "_private") {
for (size_t i = begin + 1; i < end; i++) {
if (parts[i].is_num && parts[i].num == 0) {
if (i + 1 < end)
return {i + 1, true};
break;
}
}
}
return {begin, false};
}
// Spec context entry: name components + context flags
struct SpecEntry {
std::string name;
std::vector<const char *> flags;
};
// Process a spec context: strip private, collect flags, format name
SpecEntry process_spec_context(const Components & comps, size_t begin, size_t end) {
SpecEntry entry;
auto sr = strip_private(comps, begin, end);
std::vector<const char *> seen_flags;
std::string name;
bool first = true;
for (size_t i = sr.begin; i < end; i++) {
const char * flag = match_suffix(comps[i]);
if (flag) {
// Deduplicate
bool dup = false;
for (auto f : entry.flags) { if (f == flag) { dup = true; break; } }
if (!dup) entry.flags.push_back(flag);
} else if (is_spec_index(comps[i])) {
// skip
} else {
if (!first) name += '.';
if (comps[i].is_num) name += std::to_string(comps[i].num);
else name += comps[i].str;
first = false;
}
}
entry.name = std::move(name);
return entry;
}
std::string postprocess_name(const Components & components) {
if (components.empty()) return "";
size_t n = components.size();
// --- Strip _private prefix ---
auto sr = strip_private(components, 0, n);
size_t begin = sr.begin;
bool is_private = sr.is_private;
// Copy relevant range into a working vector
Components parts(components.begin() + begin, components.begin() + n);
// --- Strip hygienic suffixes: everything from _@ onward ---
{
size_t cut = parts.size();
for (size_t i = 0; i < parts.size(); i++) {
if (!parts[i].is_num && starts_with_str(parts[i].str, "_@")) {
cut = i;
break;
}
}
parts.resize(cut);
}
// --- Handle specialization: _at_ ... _spec N ---
std::vector<SpecEntry> spec_entries;
{
// Find first _at_
int first_at = -1;
for (size_t i = 0; i < parts.size(); i++) {
if (!parts[i].is_num && parts[i].str == "_at_") {
first_at = (int)i;
break;
}
}
if (first_at >= 0) {
Components base(parts.begin(), parts.begin() + first_at);
// Parse _at_..._spec entries
Components current_ctx;
bool in_ctx = false;
Components remaining;
bool skip_next = false;
for (size_t i = first_at; i < parts.size(); i++) {
if (skip_next) { skip_next = false; continue; }
if (!parts[i].is_num && parts[i].str == "_at_") {
if (in_ctx) {
auto entry = process_spec_context(current_ctx, 0, current_ctx.size());
if (!entry.name.empty() || !entry.flags.empty())
spec_entries.push_back(std::move(entry));
current_ctx.clear();
}
in_ctx = true;
continue;
}
if (!parts[i].is_num && parts[i].str == "_spec") {
if (in_ctx) {
auto entry = process_spec_context(current_ctx, 0, current_ctx.size());
if (!entry.name.empty() || !entry.flags.empty())
spec_entries.push_back(std::move(entry));
current_ctx.clear();
in_ctx = false;
}
skip_next = true;
continue;
}
if (!parts[i].is_num && starts_with_str(parts[i].str, "_spec")) {
if (in_ctx) {
auto entry = process_spec_context(current_ctx, 0, current_ctx.size());
if (!entry.name.empty() || !entry.flags.empty())
spec_entries.push_back(std::move(entry));
current_ctx.clear();
in_ctx = false;
}
continue;
}
if (in_ctx)
current_ctx.push_back(parts[i]);
else
remaining.push_back(parts[i]);
}
if (in_ctx && !current_ctx.empty()) {
auto entry = process_spec_context(current_ctx, 0, current_ctx.size());
if (!entry.name.empty() || !entry.flags.empty())
spec_entries.push_back(std::move(entry));
}
parts = base;
parts.insert(parts.end(), remaining.begin(), remaining.end());
}
}
// --- Collect suffix flags from the end ---
std::vector<const char *> flags;
while (!parts.empty()) {
const Component & last = parts.back();
const char * flag = match_suffix(last);
if (flag) {
flags.push_back(flag);
parts.pop_back();
} else if (last.is_num && parts.size() >= 2) {
const char * prev_flag = match_suffix(parts[parts.size() - 2]);
if (prev_flag) {
flags.push_back(prev_flag);
parts.pop_back(); // number
parts.pop_back(); // suffix
} else {
break;
}
} else {
break;
}
}
if (is_private) flags.push_back("private");
// --- Format result ---
std::string result = parts.empty() ? "?" : format_name(parts);
if (!flags.empty()) {
result += " [";
for (size_t i = 0; i < flags.size(); i++) {
if (i > 0) result += ", ";
result += flags[i];
}
result += ']';
}
for (auto & entry : spec_entries) {
std::string ctx_str = entry.name.empty() ? "?" : entry.name;
if (!entry.flags.empty()) {
result += " spec at " + ctx_str + "[";
for (size_t i = 0; i < entry.flags.size(); i++) {
if (i > 0) result += ", ";
result += entry.flags[i];
}
result += ']';
} else {
result += " spec at " + ctx_str;
}
}
return result;
}
// ---------------------------------------------------------------------------
// Prefix handling and lp_ splitting
// ---------------------------------------------------------------------------
const char * starts_with(const char * s, const char * prefix) {
size_t plen = strlen(prefix);
if (strncmp(s, prefix, plen) == 0) return s + plen;
return nullptr;
}
bool has_upper_start(const char * s, int len) {
if (len == 0) return false;
int pos = 0;
if (pos + 1 < len && s[pos] == '0' && s[pos + 1] == '0') pos += 2;
while (pos < len && s[pos] == '_') pos++;
if (pos >= len) return false;
return s[pos] >= 'A' && s[pos] <= 'Z';
}
bool is_valid_string_mangle(const char * s, int end) {
int pos = 0;
while (pos < end) {
char ch = s[pos];
if ((ch >= 'a' && ch <= 'z') || (ch >= 'A' && ch <= 'Z') || (ch >= '0' && ch <= '9')) {
pos++;
} else if (ch == '_') {
if (pos + 1 >= end) return false;
char nch = s[pos + 1];
unsigned v;
if (nch == '_') { pos += 2; }
else if (nch == 'x' && parse_hex(s, pos + 2, end, 2, v)) { pos += 4; }
else if (nch == 'u' && parse_hex(s, pos + 2, end, 4, v)) { pos += 6; }
else if (nch == 'U' && parse_hex(s, pos + 2, end, 8, v)) { pos += 10; }
else return false;
} else {
return false;
}
}
return true;
}
int find_lp_body(const char * s, int len) {
int best = -1;
bool best_has_upper = false;
for (int i = 0; i < len; i++) {
if (s[i] != '_') continue;
if (i == 0) continue;
if (!is_valid_string_mangle(s, i)) continue;
int body_start = i + 1;
int body_len = len - body_start;
if (body_len <= 0) continue;
Components test;
if (!demangle_body(s + body_start, body_len, test)) continue;
bool upper = has_upper_start(s + body_start, body_len);
if (upper) {
if (!best_has_upper || i > best - 1) {
best = body_start;
best_has_upper = true;
}
} else if (!best_has_upper) {
if (best == -1) best = body_start;
}
}
return best;
}
void unmangle_pkg(const char * s, int len, std::string & out) {
std::string tmp;
if (demangle_body_flat(s, len, tmp) && tmp.find('.') == std::string::npos) {
out += tmp;
} else {
out.append(s, len);
}
}
// ---------------------------------------------------------------------------
// Helper to produce final malloc'd string
// ---------------------------------------------------------------------------
char * to_malloc_str(const std::string & s) {
char * ret = (char *)malloc(s.size() + 1);
if (ret) memcpy(ret, s.c_str(), s.size() + 1);
return ret;
}
// Demangle body and postprocess to human-friendly string.
bool demangle_and_postprocess(const char * body, int body_len, std::string & out) {
Components comps;
if (!demangle_body(body, body_len, comps)) return false;
out = postprocess_name(comps);
return true;
}
} // anonymous namespace
// ---------------------------------------------------------------------------
// Public API
// ---------------------------------------------------------------------------
char * lean_demangle_symbol(const char * symbol) {
if (!symbol || !symbol[0]) return nullptr;
int slen = (int)strlen(symbol);
// Handle lean_apply_N -> <apply/N>
{
const char * rest = starts_with(symbol, "lean_apply_");
if (rest && is_all_digits(rest)) {
std::string result = "<apply/";
result += rest;
result += '>';
return to_malloc_str(result);
}
}
// Strip .cold.N or .cold suffix
int core_len = slen;
const char * cold_suffix = nullptr;
int cold_suffix_len = 0;
for (int i = 0; i < slen; i++) {
if (symbol[i] == '.' && i + 5 <= slen && strncmp(symbol + i, ".cold", 5) == 0) {
core_len = i;
cold_suffix = symbol + i;
cold_suffix_len = slen - i;
break;
}
}
std::string core(symbol, core_len);
const char * cs = core.c_str();
// _lean_main
if (core == "_lean_main") {
std::string result = "[lean] main";
if (cold_suffix) { result += ' '; result.append(cold_suffix, cold_suffix_len); }
return to_malloc_str(result);
}
std::string out;
const char * rest;
// _init_l_ prefix
if ((rest = starts_with(cs, "_init_l_")) != nullptr) {
int body_len = core_len - (int)(rest - cs);
if (body_len > 0 && demangle_and_postprocess(rest, body_len, out)) {
std::string result = "[init] " + out;
if (cold_suffix) { result += ' '; result.append(cold_suffix, cold_suffix_len); }
return to_malloc_str(result);
}
}
// _init_lp_ prefix
if ((rest = starts_with(cs, "_init_lp_")) != nullptr) {
int after_len = core_len - (int)(rest - cs);
int body_idx = find_lp_body(rest, after_len);
if (body_idx >= 0) {
std::string pkg_out;
unmangle_pkg(rest, body_idx - 1, pkg_out);
if (demangle_and_postprocess(rest + body_idx, after_len - body_idx, out)) {
std::string result = "[init] " + out + " (" + pkg_out + ")";
if (cold_suffix) { result += ' '; result.append(cold_suffix, cold_suffix_len); }
return to_malloc_str(result);
}
}
}
// initialize_l_ prefix
if ((rest = starts_with(cs, "initialize_l_")) != nullptr) {
int body_len = core_len - (int)(rest - cs);
if (body_len > 0 && demangle_and_postprocess(rest, body_len, out)) {
std::string result = "[module_init] " + out;
if (cold_suffix) { result += ' '; result.append(cold_suffix, cold_suffix_len); }
return to_malloc_str(result);
}
}
// initialize_lp_ prefix
if ((rest = starts_with(cs, "initialize_lp_")) != nullptr) {
int after_len = core_len - (int)(rest - cs);
int body_idx = find_lp_body(rest, after_len);
if (body_idx >= 0) {
std::string pkg_out;
unmangle_pkg(rest, body_idx - 1, pkg_out);
if (demangle_and_postprocess(rest + body_idx, after_len - body_idx, out)) {
std::string result = "[module_init] " + out + " (" + pkg_out + ")";
if (cold_suffix) { result += ' '; result.append(cold_suffix, cold_suffix_len); }
return to_malloc_str(result);
}
}
}
// initialize_ (bare module init)
if ((rest = starts_with(cs, "initialize_")) != nullptr) {
int body_len = core_len - (int)(rest - cs);
if (body_len > 0 && demangle_and_postprocess(rest, body_len, out)) {
std::string result = "[module_init] " + out;
if (cold_suffix) { result += ' '; result.append(cold_suffix, cold_suffix_len); }
return to_malloc_str(result);
}
}
// l_ prefix
if ((rest = starts_with(cs, "l_")) != nullptr) {
int body_len = core_len - (int)(rest - cs);
if (body_len > 0 && demangle_and_postprocess(rest, body_len, out)) {
if (cold_suffix) { out += ' '; out.append(cold_suffix, cold_suffix_len); }
return to_malloc_str(out);
}
}
// lp_ prefix
if ((rest = starts_with(cs, "lp_")) != nullptr) {
int after_len = core_len - (int)(rest - cs);
int body_idx = find_lp_body(rest, after_len);
if (body_idx >= 0) {
std::string pkg_out;
unmangle_pkg(rest, body_idx - 1, pkg_out);
if (demangle_and_postprocess(rest + body_idx, after_len - body_idx, out)) {
std::string result = out + " (" + pkg_out + ")";
if (cold_suffix) { result += ' '; result.append(cold_suffix, cold_suffix_len); }
return to_malloc_str(result);
}
}
}
return nullptr;
}
// ---------------------------------------------------------------------------
// Backtrace line parsing
// ---------------------------------------------------------------------------
static const char * extract_symbol(const char * line, int * sym_len) {
int len = (int)strlen(line);
// Linux (glibc): ./lean(l_Lean_Meta_foo+0x2a) [0x555...]
for (int i = 0; i < len; i++) {
if (line[i] == '(') {
int start = i + 1;
for (int j = start; j < len; j++) {
if (line[j] == '+' || line[j] == ')') {
if (j > start) { *sym_len = j - start; return line + start; }
break;
}
}
break;
}
}
// macOS: 2 lean 0x100abc123 l_Lean_Meta_foo + 42
for (int i = 0; i + 1 < len; i++) {
if (line[i] == '0' && line[i + 1] == 'x') {
int j = i + 2;
while (j < len && ((line[j] >= '0' && line[j] <= '9') ||
(line[j] >= 'a' && line[j] <= 'f') ||
(line[j] >= 'A' && line[j] <= 'F'))) j++;
while (j < len && line[j] == ' ') j++;
if (j >= len) return nullptr;
int start = j;
while (j < len) {
if (j + 2 < len && line[j] == ' ' && line[j + 1] == '+' && line[j + 2] == ' ')
break;
j++;
}
if (j > start) { *sym_len = j - start; return line + start; }
return nullptr;
}
}
return nullptr;
}
char * lean_demangle_bt_line(const char * line) {
if (!line) return nullptr;
int sym_len = 0;
const char * sym = extract_symbol(line, &sym_len);
if (!sym || sym_len == 0) return nullptr;
// Make null-terminated copy
char * sym_copy = (char *)malloc(sym_len + 1);
if (!sym_copy) return nullptr;
memcpy(sym_copy, sym, sym_len);
sym_copy[sym_len] = '\0';
char * demangled = lean_demangle_symbol(sym_copy);
free(sym_copy);
if (!demangled) return nullptr;
// Reconstruct line with demangled name
int line_len = (int)strlen(line);
int dem_len = (int)strlen(demangled);
int prefix_len = (int)(sym - line);
int suffix_start = prefix_len + sym_len;
int suffix_len = line_len - suffix_start;
int new_len = prefix_len + dem_len + suffix_len;
char * result = (char *)malloc(new_len + 1);
if (!result) { free(demangled); return nullptr; }
memcpy(result, line, prefix_len);
memcpy(result + prefix_len, demangled, dem_len);
memcpy(result + prefix_len + dem_len, line + suffix_start, suffix_len);
result[new_len] = '\0';
free(demangled);
return result;
}

26
stage0/src/runtime/demangle.h generated
View file

@ -1,26 +0,0 @@
/*
Copyright (c) 2025 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
/*
* Demangle Lean symbol names in backtrace lines.
*
* lean_demangle_symbol(symbol):
* Given a mangled C symbol name (e.g. "l_Lean_Meta_Grind_foo"),
* returns a malloc'd string with the demangled name (e.g. "Lean.Meta.Grind.foo"),
* or nullptr if the symbol is not a Lean name.
*
* lean_demangle_bt_line(line):
* Given a backtrace line from backtrace_symbols(), extracts the symbol,
* demangles it, and returns a malloc'd string with the demangled name
* substituted in. Returns nullptr if nothing was demangled.
*
* Callers must free() non-null return values.
*/
char * lean_demangle_symbol(const char * symbol);
char * lean_demangle_bt_line(const char * line);

27
stage0/src/runtime/object.cpp generated
View file

@ -31,7 +31,13 @@ Author: Leonardo de Moura
#if LEAN_SUPPORTS_BACKTRACE
#include <execinfo.h>
#include <unistd.h>
#include "runtime/demangle.h"
// Lean-exported demangler from Lean.Compiler.NameDemangling.
// Declared as a weak symbol so leanrt doesn't require libLean at link time.
// When the Lean demangler is linked in, it overrides this stub.
extern "C" __attribute__((weak)) lean_object * lean_demangle_bt_line_cstr(lean_object * s) {
lean_dec(s);
return lean_mk_string("");
}
#endif
// HACK: for unknown reasons, std::isnan(x) fails on msys64 because math.h
@ -137,13 +143,20 @@ static void print_backtrace(bool force_stderr) {
if (char ** symbols = backtrace_symbols(bt_buf, nptrs)) {
bool raw = getenv("LEAN_BACKTRACE_RAW");
for (int i = 0; i < nptrs; i++) {
char * demangled = raw ? nullptr : lean_demangle_bt_line(symbols[i]);
if (demangled) {
panic_eprintln(demangled, force_stderr);
free(demangled);
} else {
panic_eprintln(symbols[i], force_stderr);
if (!raw) {
lean_object * line_obj = lean_mk_string(symbols[i]);
lean_object * result = lean_demangle_bt_line_cstr(line_obj);
char const * result_str = lean_string_cstr(result);
if (result_str[0] != '\0') {
panic_eprintln(result_str, force_stderr);
lean_dec(result);
lean_dec(line_obj);
continue;
}
lean_dec(result);
lean_dec(line_obj);
}
panic_eprintln(symbols[i], force_stderr);
}
// According to `man backtrace`, each `symbols[i]` should NOT be freed
free(symbols);

2
stage0/src/stdlib_flags.h
View file

@ -1,7 +1,5 @@
#include "util/options.h"
// Dear CI, please build stage 2 first
namespace lean {
options get_default_options() {
options opts;

12
stage0/stdlib/Init/Data/Array.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Data.Array
// Imports: public import Init.Data.Array.Basic public import Init.Data.Array.QSort public import Init.Data.Array.BinSearch public import Init.Data.Array.InsertionSort public import Init.Data.Array.DecidableEq public import Init.Data.Array.Mem public import Init.Data.Array.Attach public import Init.Data.Array.BasicAux public import Init.Data.Array.Lemmas public import Init.Data.Array.TakeDrop public import Init.Data.Array.Bootstrap public import Init.Data.Array.GetLit public import Init.Data.Array.MapIdx public import Init.Data.Array.Set public import Init.Data.Array.Monadic public import Init.Data.Array.FinRange public import Init.Data.Array.Perm public import Init.Data.Array.Find public import Init.Data.Array.Lex public import Init.Data.Array.Range public import Init.Data.Array.Erase public import Init.Data.Array.Zip public import Init.Data.Array.InsertIdx public import Init.Data.Array.Extract public import Init.Data.Array.MinMax public import Init.Data.Array.Nat public import Init.Data.Array.Int public import Init.Data.Array.Count
// Imports: public import Init.Data.Array.Basic public import Init.Data.Array.QSort public import Init.Data.Array.BinSearch public import Init.Data.Array.InsertionSort public import Init.Data.Array.DecidableEq public import Init.Data.Array.Mem public import Init.Data.Array.Attach public import Init.Data.Array.BasicAux public import Init.Data.Array.Lemmas public import Init.Data.Array.TakeDrop public import Init.Data.Array.Bootstrap public import Init.Data.Array.GetLit public import Init.Data.Array.MapIdx public import Init.Data.Array.Set public import Init.Data.Array.Monadic public import Init.Data.Array.FinRange public import Init.Data.Array.Perm public import Init.Data.Array.Find public import Init.Data.Array.Lex public import Init.Data.Array.Range public import Init.Data.Array.Erase public import Init.Data.Array.Zip public import Init.Data.Array.InsertIdx public import Init.Data.Array.Extract public import Init.Data.Array.MinMax public import Init.Data.Array.Nat public import Init.Data.Array.Int public import Init.Data.Array.Count public import Init.Data.Array.Sort
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -41,6 +41,7 @@ lean_object* runtime_initialize_Init_Data_Array_MinMax(uint8_t builtin);
lean_object* runtime_initialize_Init_Data_Array_Nat(uint8_t builtin);
lean_object* runtime_initialize_Init_Data_Array_Int(uint8_t builtin);
lean_object* runtime_initialize_Init_Data_Array_Count(uint8_t builtin);
lean_object* runtime_initialize_Init_Data_Array_Sort(uint8_t builtin);
static bool _G_runtime_initialized = false;
LEAN_EXPORT lean_object* runtime_initialize_Init_Data_Array(uint8_t builtin) {
lean_object * res;
@ -158,6 +159,10 @@ res = runtime_initialize_Init_Data_Array_Count(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Init_Data_Array_Sort(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;
@ -195,6 +200,7 @@ lean_object* initialize_Init_Data_Array_MinMax(uint8_t builtin);
lean_object* initialize_Init_Data_Array_Nat(uint8_t builtin);
lean_object* initialize_Init_Data_Array_Int(uint8_t builtin);
lean_object* initialize_Init_Data_Array_Count(uint8_t builtin);
lean_object* initialize_Init_Data_Array_Sort(uint8_t builtin);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Init_Data_Array(uint8_t builtin) {
lean_object * res;
@ -312,6 +318,10 @@ res = initialize_Init_Data_Array_Count(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Array_Sort(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Init_Data_Array(builtin)
;
if (lean_io_result_is_error(res)) return res;

67
stage0/stdlib/Init/Data/Array/Sort.c generated Normal file
View file

@ -0,0 +1,67 @@
// Lean compiler output
// Module: Init.Data.Array.Sort
// Imports: public import Init.Data.Array.Sort.Basic public import Init.Data.Array.Sort.Lemmas
#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* runtime_initialize_Init_Data_Array_Sort_Basic(uint8_t builtin);
lean_object* runtime_initialize_Init_Data_Array_Sort_Lemmas(uint8_t builtin);
static bool _G_runtime_initialized = false;
LEAN_EXPORT lean_object* runtime_initialize_Init_Data_Array_Sort(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_Init_Data_Array_Sort_Basic(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Init_Data_Array_Sort_Lemmas(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_Init_Data_Array_Sort(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_Init_Data_Array_Sort_Basic(uint8_t builtin);
lean_object* initialize_Init_Data_Array_Sort_Lemmas(uint8_t builtin);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Init_Data_Array_Sort(uint8_t builtin) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init_Data_Array_Sort_Basic(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Array_Sort_Lemmas(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Init_Data_Array_Sort(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = meta_initialize_Init_Data_Array_Sort(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return initialize_Init_Data_Array_Sort(builtin);
}
#ifdef __cplusplus
}
#endif

1058
stage0/stdlib/Init/Data/Array/Sort/Basic.c generated Normal file
View file

File diff suppressed because it is too large Load diff

306
stage0/stdlib/Init/Data/Array/Sort/Lemmas.c generated Normal file
View file

@ -0,0 +1,306 @@
// Lean compiler output
// Module: Init.Data.Array.Sort.Lemmas
// Imports: public import Init.Data.Array.Sort.Basic public import Init.Data.List.Sort.Basic public import Init.Data.Array.Perm import all Init.Data.Array.Sort.Basic import all Init.Data.List.Sort.Basic import Init.Data.List.Sort.Lemmas import Init.Data.Slice.Array.Lemmas import Init.Data.Slice.List.Lemmas import Init.Data.Array.Bootstrap import Init.Data.Array.Lemmas import Init.Data.Array.MapIdx import Init.ByCases
#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_EXPORT lean_object* l___private_Init_Data_Array_Sort_Lemmas_0__List_merge_match__1_splitter___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Sort_Lemmas_0__List_merge_match__1_splitter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Sort_Lemmas_0__List_mergeSort_match__1_splitter___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Sort_Lemmas_0__List_mergeSort_match__1_splitter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Sort_Lemmas_0__List_merge_match__1_splitter___redArg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
lean_object* x_6;
lean_dec(x_5);
lean_dec(x_4);
x_6 = lean_apply_1(x_3, x_2);
return x_6;
}
else
{
lean_dec(x_3);
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_7;
lean_dec(x_5);
x_7 = lean_apply_2(x_4, x_1, lean_box(0));
return x_7;
}
else
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
lean_dec(x_4);
x_8 = lean_ctor_get(x_1, 0);
lean_inc(x_8);
x_9 = lean_ctor_get(x_1, 1);
lean_inc(x_9);
lean_dec_ref(x_1);
x_10 = lean_ctor_get(x_2, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_2, 1);
lean_inc(x_11);
lean_dec_ref(x_2);
x_12 = lean_apply_4(x_5, x_8, x_9, x_10, x_11);
return x_12;
}
}
}
}
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Sort_Lemmas_0__List_merge_match__1_splitter(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
if (lean_obj_tag(x_3) == 0)
{
lean_object* x_8;
lean_dec(x_7);
lean_dec(x_6);
x_8 = lean_apply_1(x_5, x_4);
return x_8;
}
else
{
lean_dec(x_5);
if (lean_obj_tag(x_4) == 0)
{
lean_object* x_9;
lean_dec(x_7);
x_9 = lean_apply_2(x_6, x_3, lean_box(0));
return x_9;
}
else
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
lean_dec(x_6);
x_10 = lean_ctor_get(x_3, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_3, 1);
lean_inc(x_11);
lean_dec_ref(x_3);
x_12 = lean_ctor_get(x_4, 0);
lean_inc(x_12);
x_13 = lean_ctor_get(x_4, 1);
lean_inc(x_13);
lean_dec_ref(x_4);
x_14 = lean_apply_4(x_7, x_10, x_11, x_12, x_13);
return x_14;
}
}
}
}
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Sort_Lemmas_0__List_mergeSort_match__1_splitter___redArg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
lean_object* x_6;
lean_dec(x_5);
lean_dec(x_4);
x_6 = lean_apply_1(x_3, x_2);
return x_6;
}
else
{
lean_object* x_7;
lean_dec(x_3);
x_7 = lean_ctor_get(x_1, 1);
if (lean_obj_tag(x_7) == 0)
{
lean_object* x_8; lean_object* x_9;
lean_dec(x_5);
x_8 = lean_ctor_get(x_1, 0);
lean_inc(x_8);
lean_dec_ref(x_1);
x_9 = lean_apply_2(x_4, x_8, x_2);
return x_9;
}
else
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
lean_inc_ref(x_7);
lean_dec(x_4);
x_10 = lean_ctor_get(x_1, 0);
lean_inc(x_10);
lean_dec_ref(x_1);
x_11 = lean_ctor_get(x_7, 0);
lean_inc(x_11);
x_12 = lean_ctor_get(x_7, 1);
lean_inc(x_12);
lean_dec_ref(x_7);
x_13 = lean_apply_4(x_5, x_10, x_11, x_12, x_2);
return x_13;
}
}
}
}
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Sort_Lemmas_0__List_mergeSort_match__1_splitter(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8;
x_8 = l___private_Init_Data_Array_Sort_Lemmas_0__List_mergeSort_match__1_splitter___redArg(x_3, x_4, x_5, x_6, x_7);
return x_8;
}
}
lean_object* runtime_initialize_Init_Data_Array_Sort_Basic(uint8_t builtin);
lean_object* runtime_initialize_Init_Data_List_Sort_Basic(uint8_t builtin);
lean_object* runtime_initialize_Init_Data_Array_Perm(uint8_t builtin);
lean_object* runtime_initialize_Init_Data_Array_Sort_Basic(uint8_t builtin);
lean_object* runtime_initialize_Init_Data_List_Sort_Basic(uint8_t builtin);
lean_object* runtime_initialize_Init_Data_List_Sort_Lemmas(uint8_t builtin);
lean_object* runtime_initialize_Init_Data_Slice_Array_Lemmas(uint8_t builtin);
lean_object* runtime_initialize_Init_Data_Slice_List_Lemmas(uint8_t builtin);
lean_object* runtime_initialize_Init_Data_Array_Bootstrap(uint8_t builtin);
lean_object* runtime_initialize_Init_Data_Array_Lemmas(uint8_t builtin);
lean_object* runtime_initialize_Init_Data_Array_MapIdx(uint8_t builtin);
lean_object* runtime_initialize_Init_ByCases(uint8_t builtin);
static bool _G_runtime_initialized = false;
LEAN_EXPORT lean_object* runtime_initialize_Init_Data_Array_Sort_Lemmas(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_Init_Data_Array_Sort_Basic(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Init_Data_List_Sort_Basic(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Init_Data_Array_Perm(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Init_Data_Array_Sort_Basic(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Init_Data_List_Sort_Basic(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Init_Data_List_Sort_Lemmas(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Init_Data_Slice_Array_Lemmas(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Init_Data_Slice_List_Lemmas(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Init_Data_Array_Bootstrap(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Init_Data_Array_Lemmas(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Init_Data_Array_MapIdx(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Init_ByCases(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_Init_Data_Array_Sort_Lemmas(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_Init_Data_Array_Sort_Basic(uint8_t builtin);
lean_object* initialize_Init_Data_List_Sort_Basic(uint8_t builtin);
lean_object* initialize_Init_Data_Array_Perm(uint8_t builtin);
lean_object* initialize_Init_Data_Array_Sort_Basic(uint8_t builtin);
lean_object* initialize_Init_Data_List_Sort_Basic(uint8_t builtin);
lean_object* initialize_Init_Data_List_Sort_Lemmas(uint8_t builtin);
lean_object* initialize_Init_Data_Slice_Array_Lemmas(uint8_t builtin);
lean_object* initialize_Init_Data_Slice_List_Lemmas(uint8_t builtin);
lean_object* initialize_Init_Data_Array_Bootstrap(uint8_t builtin);
lean_object* initialize_Init_Data_Array_Lemmas(uint8_t builtin);
lean_object* initialize_Init_Data_Array_MapIdx(uint8_t builtin);
lean_object* initialize_Init_ByCases(uint8_t builtin);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Init_Data_Array_Sort_Lemmas(uint8_t builtin) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init_Data_Array_Sort_Basic(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_List_Sort_Basic(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Array_Perm(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Array_Sort_Basic(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_List_Sort_Basic(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_List_Sort_Lemmas(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Slice_Array_Lemmas(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Slice_List_Lemmas(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Array_Bootstrap(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Array_Lemmas(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Array_MapIdx(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_ByCases(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Init_Data_Array_Sort_Lemmas(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = meta_initialize_Init_Data_Array_Sort_Lemmas(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return initialize_Init_Data_Array_Sort_Lemmas(builtin);
}
#ifdef __cplusplus
}
#endif

84
stage0/stdlib/Init/Data/Char/Basic.c generated
View file

@ -42,6 +42,8 @@ LEAN_EXPORT uint8_t l_Char_isAlpha(uint32_t);
LEAN_EXPORT lean_object* l_Char_isAlpha___boxed(lean_object*);
LEAN_EXPORT uint8_t l_Char_isDigit(uint32_t);
LEAN_EXPORT lean_object* l_Char_isDigit___boxed(lean_object*);
LEAN_EXPORT uint8_t l_Char_isHexDigit(uint32_t);
LEAN_EXPORT lean_object* l_Char_isHexDigit___boxed(lean_object*);
LEAN_EXPORT uint8_t l_Char_isAlphanum(uint32_t);
LEAN_EXPORT lean_object* l_Char_isAlphanum___boxed(lean_object*);
uint32_t lean_uint32_add(uint32_t, uint32_t);
@ -370,6 +372,88 @@ x_4 = lean_box(x_3);
return x_4;
}
}
LEAN_EXPORT uint8_t l_Char_isHexDigit(uint32_t x_1) {
_start:
{
uint8_t x_2; uint8_t x_8; uint32_t x_14; uint8_t x_15;
x_14 = 48;
x_15 = lean_uint32_dec_le(x_14, x_1);
if (x_15 == 0)
{
x_8 = x_15;
goto block_13;
}
else
{
uint32_t x_16; uint8_t x_17;
x_16 = 57;
x_17 = lean_uint32_dec_le(x_1, x_16);
x_8 = x_17;
goto block_13;
}
block_7:
{
if (x_2 == 0)
{
uint32_t x_3; uint8_t x_4;
x_3 = 65;
x_4 = lean_uint32_dec_le(x_3, x_1);
if (x_4 == 0)
{
return x_4;
}
else
{
uint32_t x_5; uint8_t x_6;
x_5 = 70;
x_6 = lean_uint32_dec_le(x_1, x_5);
return x_6;
}
}
else
{
return x_2;
}
}
block_13:
{
if (x_8 == 0)
{
uint32_t x_9; uint8_t x_10;
x_9 = 97;
x_10 = lean_uint32_dec_le(x_9, x_1);
if (x_10 == 0)
{
x_2 = x_10;
goto block_7;
}
else
{
uint32_t x_11; uint8_t x_12;
x_11 = 102;
x_12 = lean_uint32_dec_le(x_1, x_11);
x_2 = x_12;
goto block_7;
}
}
else
{
return x_8;
}
}
}
}
LEAN_EXPORT lean_object* l_Char_isHexDigit___boxed(lean_object* x_1) {
_start:
{
uint32_t x_2; uint8_t x_3; lean_object* x_4;
x_2 = lean_unbox_uint32(x_1);
lean_dec(x_1);
x_3 = l_Char_isHexDigit(x_2);
x_4 = lean_box(x_3);
return x_4;
}
}
LEAN_EXPORT uint8_t l_Char_isAlphanum(uint32_t x_1) {
_start:
{

854
stage0/stdlib/Init/Data/Order/PackageFactories.c generated
View file

@ -3369,9 +3369,36 @@ return x_5;
LEAN_EXPORT uint8_t l_Std_FactoryInstances_decidableLTOfLE(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
uint8_t x_8;
x_8 = l_Std_FactoryInstances_decidableLTOfLE___redArg(x_4, x_6, x_7);
return x_8;
lean_object* x_8; lean_object* x_9; uint8_t x_10;
lean_inc_ref(x_4);
lean_inc(x_6);
lean_inc(x_7);
x_8 = lean_apply_2(x_4, x_7, x_6);
x_9 = lean_apply_2(x_4, x_6, x_7);
x_10 = lean_unbox(x_9);
if (x_10 == 0)
{
uint8_t x_11;
x_11 = lean_unbox(x_9);
return x_11;
}
else
{
uint8_t x_12;
x_12 = lean_unbox(x_8);
if (x_12 == 0)
{
uint8_t x_13;
x_13 = lean_unbox(x_9);
return x_13;
}
else
{
uint8_t x_14;
x_14 = 0;
return x_14;
}
}
}
}
LEAN_EXPORT lean_object* l_Std_FactoryInstances_decidableLTOfLE___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
@ -9034,9 +9061,59 @@ return x_9;
LEAN_EXPORT lean_object* l_Std_PreorderPackage_ofLE(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Std_PreorderPackage_ofLE___redArg(x_2);
return x_3;
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9; uint8_t x_14;
x_3 = lean_ctor_get(x_2, 0);
x_4 = lean_ctor_get(x_2, 1);
x_5 = lean_ctor_get(x_2, 2);
x_6 = lean_ctor_get(x_2, 3);
x_7 = lean_ctor_get(x_2, 4);
x_14 = !lean_is_exclusive(x_2);
if (x_14 == 0)
{
x_8 = x_2;
x_9 = x_14;
goto block_13;
}
else
{
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_dec(x_2);
x_8 = lean_box(0);
x_9 = x_14;
goto block_13;
}
block_13:
{
lean_object* x_10;
if (x_9 == 0)
{
lean_ctor_set(x_8, 3, x_4);
lean_ctor_set(x_8, 2, x_6);
lean_ctor_set(x_8, 1, x_5);
x_10 = x_8;
goto block_11;
}
else
{
lean_object* x_12;
x_12 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_12, 0, x_3);
lean_ctor_set(x_12, 1, x_5);
lean_ctor_set(x_12, 2, x_6);
lean_ctor_set(x_12, 3, x_4);
lean_ctor_set(x_12, 4, x_7);
x_10 = x_12;
goto block_11;
}
block_11:
{
return x_10;
}
}
}
}
static lean_object* _init_l_Std_Packages_PartialOrderOfLEArgs_le__antisymm___autoParam___closed__1(void) {
@ -9524,17 +9601,117 @@ return x_1;
LEAN_EXPORT lean_object* l_Std_PartialOrderPackage_ofLE___redArg(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Std_PreorderPackage_ofLE___redArg(x_1);
return x_2;
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8; uint8_t x_13;
x_2 = lean_ctor_get(x_1, 0);
x_3 = lean_ctor_get(x_1, 1);
x_4 = lean_ctor_get(x_1, 2);
x_5 = lean_ctor_get(x_1, 3);
x_6 = lean_ctor_get(x_1, 4);
x_13 = !lean_is_exclusive(x_1);
if (x_13 == 0)
{
x_7 = x_1;
x_8 = x_13;
goto block_12;
}
else
{
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
lean_dec(x_1);
x_7 = lean_box(0);
x_8 = x_13;
goto block_12;
}
block_12:
{
lean_object* x_9;
if (x_8 == 0)
{
lean_ctor_set(x_7, 3, x_3);
lean_ctor_set(x_7, 2, x_5);
lean_ctor_set(x_7, 1, x_4);
x_9 = x_7;
goto block_10;
}
else
{
lean_object* x_11;
x_11 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_11, 0, x_2);
lean_ctor_set(x_11, 1, x_4);
lean_ctor_set(x_11, 2, x_5);
lean_ctor_set(x_11, 3, x_3);
lean_ctor_set(x_11, 4, x_6);
x_9 = x_11;
goto block_10;
}
block_10:
{
return x_9;
}
}
}
}
LEAN_EXPORT lean_object* l_Std_PartialOrderPackage_ofLE(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Std_PreorderPackage_ofLE___redArg(x_2);
return x_3;
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9; uint8_t x_14;
x_3 = lean_ctor_get(x_2, 0);
x_4 = lean_ctor_get(x_2, 1);
x_5 = lean_ctor_get(x_2, 2);
x_6 = lean_ctor_get(x_2, 3);
x_7 = lean_ctor_get(x_2, 4);
x_14 = !lean_is_exclusive(x_2);
if (x_14 == 0)
{
x_8 = x_2;
x_9 = x_14;
goto block_13;
}
else
{
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_dec(x_2);
x_8 = lean_box(0);
x_9 = x_14;
goto block_13;
}
block_13:
{
lean_object* x_10;
if (x_9 == 0)
{
lean_ctor_set(x_8, 3, x_4);
lean_ctor_set(x_8, 2, x_6);
lean_ctor_set(x_8, 1, x_5);
x_10 = x_8;
goto block_11;
}
else
{
lean_object* x_12;
x_12 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_12, 0, x_3);
lean_ctor_set(x_12, 1, x_5);
lean_ctor_set(x_12, 2, x_6);
lean_ctor_set(x_12, 3, x_4);
lean_ctor_set(x_12, 4, x_7);
x_10 = x_12;
goto block_11;
}
block_11:
{
return x_10;
}
}
}
}
LEAN_EXPORT uint8_t l_Std_FactoryInstances_instOrdOfDecidableLE___redArg___lam__0(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
@ -11322,15 +11499,15 @@ return x_1;
LEAN_EXPORT lean_object* l_Std_LinearPreorderPackage_ofLE___redArg(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; uint8_t x_5; uint8_t x_11;
lean_object* x_2; lean_object* x_3; lean_object* x_4; uint8_t x_5; uint8_t x_22;
x_2 = lean_ctor_get(x_1, 0);
x_3 = lean_ctor_get(x_1, 1);
x_11 = !lean_is_exclusive(x_1);
if (x_11 == 0)
x_22 = !lean_is_exclusive(x_1);
if (x_22 == 0)
{
x_4 = x_1;
x_5 = x_11;
goto block_10;
x_5 = x_22;
goto block_21;
}
else
{
@ -11338,31 +11515,82 @@ lean_inc(x_3);
lean_inc(x_2);
lean_dec(x_1);
x_4 = lean_box(0);
x_5 = x_11;
goto block_10;
x_5 = x_22;
goto block_21;
}
block_10:
block_21:
{
lean_object* x_6; lean_object* x_7;
x_6 = l_Std_PreorderPackage_ofLE___redArg(x_2);
if (x_5 == 0)
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12; uint8_t x_20;
x_6 = lean_ctor_get(x_2, 0);
x_7 = lean_ctor_get(x_2, 1);
x_8 = lean_ctor_get(x_2, 2);
x_9 = lean_ctor_get(x_2, 3);
x_10 = lean_ctor_get(x_2, 4);
x_20 = !lean_is_exclusive(x_2);
if (x_20 == 0)
{
lean_ctor_set(x_4, 0, x_6);
x_7 = x_4;
goto block_8;
x_11 = x_2;
x_12 = x_20;
goto block_19;
}
else
{
lean_object* x_9;
x_9 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_9, 0, x_6);
lean_ctor_set(x_9, 1, x_3);
x_7 = x_9;
goto block_8;
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_dec(x_2);
x_11 = lean_box(0);
x_12 = x_20;
goto block_19;
}
block_8:
block_19:
{
return x_7;
lean_object* x_13;
if (x_12 == 0)
{
lean_ctor_set(x_11, 3, x_7);
lean_ctor_set(x_11, 2, x_9);
lean_ctor_set(x_11, 1, x_8);
x_13 = x_11;
goto block_17;
}
else
{
lean_object* x_18;
x_18 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_18, 0, x_6);
lean_ctor_set(x_18, 1, x_8);
lean_ctor_set(x_18, 2, x_9);
lean_ctor_set(x_18, 3, x_7);
lean_ctor_set(x_18, 4, x_10);
x_13 = x_18;
goto block_17;
}
block_17:
{
lean_object* x_14;
if (x_5 == 0)
{
lean_ctor_set(x_4, 0, x_13);
x_14 = x_4;
goto block_15;
}
else
{
lean_object* x_16;
x_16 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_16, 0, x_13);
lean_ctor_set(x_16, 1, x_3);
x_14 = x_16;
goto block_15;
}
block_15:
{
return x_14;
}
}
}
}
}
@ -11370,9 +11598,100 @@ return x_7;
LEAN_EXPORT lean_object* l_Std_LinearPreorderPackage_ofLE(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Std_LinearPreorderPackage_ofLE___redArg(x_2);
return x_3;
lean_object* x_3; lean_object* x_4; lean_object* x_5; uint8_t x_6; uint8_t x_23;
x_3 = lean_ctor_get(x_2, 0);
x_4 = lean_ctor_get(x_2, 1);
x_23 = !lean_is_exclusive(x_2);
if (x_23 == 0)
{
x_5 = x_2;
x_6 = x_23;
goto block_22;
}
else
{
lean_inc(x_4);
lean_inc(x_3);
lean_dec(x_2);
x_5 = lean_box(0);
x_6 = x_23;
goto block_22;
}
block_22:
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; uint8_t x_13; uint8_t x_21;
x_7 = lean_ctor_get(x_3, 0);
x_8 = lean_ctor_get(x_3, 1);
x_9 = lean_ctor_get(x_3, 2);
x_10 = lean_ctor_get(x_3, 3);
x_11 = lean_ctor_get(x_3, 4);
x_21 = !lean_is_exclusive(x_3);
if (x_21 == 0)
{
x_12 = x_3;
x_13 = x_21;
goto block_20;
}
else
{
lean_inc(x_11);
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_dec(x_3);
x_12 = lean_box(0);
x_13 = x_21;
goto block_20;
}
block_20:
{
lean_object* x_14;
if (x_13 == 0)
{
lean_ctor_set(x_12, 3, x_8);
lean_ctor_set(x_12, 2, x_10);
lean_ctor_set(x_12, 1, x_9);
x_14 = x_12;
goto block_18;
}
else
{
lean_object* x_19;
x_19 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_19, 0, x_7);
lean_ctor_set(x_19, 1, x_9);
lean_ctor_set(x_19, 2, x_10);
lean_ctor_set(x_19, 3, x_8);
lean_ctor_set(x_19, 4, x_11);
x_14 = x_19;
goto block_18;
}
block_18:
{
lean_object* x_15;
if (x_6 == 0)
{
lean_ctor_set(x_5, 0, x_14);
x_15 = x_5;
goto block_16;
}
else
{
lean_object* x_17;
x_17 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_17, 0, x_14);
lean_ctor_set(x_17, 1, x_4);
x_15 = x_17;
goto block_16;
}
block_16:
{
return x_15;
}
}
}
}
}
}
LEAN_EXPORT lean_object* l_Std_LinearOrderPackage_toPartialOrderPackage___redArg(lean_object* x_1) {
@ -13510,50 +13829,148 @@ return x_1;
LEAN_EXPORT lean_object* l_Std_LinearOrderPackage_ofLE___redArg(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; uint8_t x_6; uint8_t x_12;
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7; uint8_t x_33;
x_2 = lean_ctor_get(x_1, 0);
x_3 = lean_ctor_get(x_1, 1);
x_4 = lean_ctor_get(x_1, 2);
x_12 = !lean_is_exclusive(x_1);
if (x_12 == 0)
lean_inc_ref(x_2);
x_3 = lean_ctor_get(x_2, 0);
lean_inc_ref(x_3);
x_4 = lean_ctor_get(x_1, 1);
x_5 = lean_ctor_get(x_1, 2);
x_33 = !lean_is_exclusive(x_1);
if (x_33 == 0)
{
x_5 = x_1;
x_6 = x_12;
goto block_11;
lean_object* x_34;
x_34 = lean_ctor_get(x_1, 0);
lean_dec(x_34);
x_6 = x_1;
x_7 = x_33;
goto block_32;
}
else
{
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
lean_dec(x_1);
x_5 = lean_box(0);
x_6 = x_12;
goto block_11;
x_6 = lean_box(0);
x_7 = x_33;
goto block_32;
}
block_11:
block_32:
{
lean_object* x_7; lean_object* x_8;
x_7 = l_Std_LinearPreorderPackage_ofLE___redArg(x_2);
if (x_6 == 0)
lean_object* x_8; lean_object* x_9; uint8_t x_10; uint8_t x_30;
x_8 = lean_ctor_get(x_2, 1);
x_30 = !lean_is_exclusive(x_2);
if (x_30 == 0)
{
lean_ctor_set(x_5, 0, x_7);
x_8 = x_5;
goto block_9;
lean_object* x_31;
x_31 = lean_ctor_get(x_2, 0);
lean_dec(x_31);
x_9 = x_2;
x_10 = x_30;
goto block_29;
}
else
{
lean_object* x_10;
x_10 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_10, 0, x_7);
lean_ctor_set(x_10, 1, x_3);
lean_ctor_set(x_10, 2, x_4);
x_8 = x_10;
goto block_9;
lean_inc(x_8);
lean_dec(x_2);
x_9 = lean_box(0);
x_10 = x_30;
goto block_29;
}
block_9:
block_29:
{
return x_8;
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; uint8_t x_17; uint8_t x_28;
x_11 = lean_ctor_get(x_3, 0);
x_12 = lean_ctor_get(x_3, 1);
x_13 = lean_ctor_get(x_3, 2);
x_14 = lean_ctor_get(x_3, 3);
x_15 = lean_ctor_get(x_3, 4);
x_28 = !lean_is_exclusive(x_3);
if (x_28 == 0)
{
x_16 = x_3;
x_17 = x_28;
goto block_27;
}
else
{
lean_inc(x_15);
lean_inc(x_14);
lean_inc(x_13);
lean_inc(x_12);
lean_inc(x_11);
lean_dec(x_3);
x_16 = lean_box(0);
x_17 = x_28;
goto block_27;
}
block_27:
{
lean_object* x_18;
if (x_17 == 0)
{
lean_ctor_set(x_16, 3, x_12);
lean_ctor_set(x_16, 2, x_14);
lean_ctor_set(x_16, 1, x_13);
x_18 = x_16;
goto block_25;
}
else
{
lean_object* x_26;
x_26 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_26, 0, x_11);
lean_ctor_set(x_26, 1, x_13);
lean_ctor_set(x_26, 2, x_14);
lean_ctor_set(x_26, 3, x_12);
lean_ctor_set(x_26, 4, x_15);
x_18 = x_26;
goto block_25;
}
block_25:
{
lean_object* x_19;
if (x_10 == 0)
{
lean_ctor_set(x_9, 0, x_18);
x_19 = x_9;
goto block_23;
}
else
{
lean_object* x_24;
x_24 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_24, 0, x_18);
lean_ctor_set(x_24, 1, x_8);
x_19 = x_24;
goto block_23;
}
block_23:
{
lean_object* x_20;
if (x_7 == 0)
{
lean_ctor_set(x_6, 0, x_19);
x_20 = x_6;
goto block_21;
}
else
{
lean_object* x_22;
x_22 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_22, 0, x_19);
lean_ctor_set(x_22, 1, x_4);
lean_ctor_set(x_22, 2, x_5);
x_20 = x_22;
goto block_21;
}
block_21:
{
return x_20;
}
}
}
}
}
}
}
@ -13561,9 +13978,150 @@ return x_8;
LEAN_EXPORT lean_object* l_Std_LinearOrderPackage_ofLE(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Std_LinearOrderPackage_ofLE___redArg(x_2);
return x_3;
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8; uint8_t x_34;
x_3 = lean_ctor_get(x_2, 0);
lean_inc_ref(x_3);
x_4 = lean_ctor_get(x_3, 0);
lean_inc_ref(x_4);
x_5 = lean_ctor_get(x_2, 1);
x_6 = lean_ctor_get(x_2, 2);
x_34 = !lean_is_exclusive(x_2);
if (x_34 == 0)
{
lean_object* x_35;
x_35 = lean_ctor_get(x_2, 0);
lean_dec(x_35);
x_7 = x_2;
x_8 = x_34;
goto block_33;
}
else
{
lean_inc(x_6);
lean_inc(x_5);
lean_dec(x_2);
x_7 = lean_box(0);
x_8 = x_34;
goto block_33;
}
block_33:
{
lean_object* x_9; lean_object* x_10; uint8_t x_11; uint8_t x_31;
x_9 = lean_ctor_get(x_3, 1);
x_31 = !lean_is_exclusive(x_3);
if (x_31 == 0)
{
lean_object* x_32;
x_32 = lean_ctor_get(x_3, 0);
lean_dec(x_32);
x_10 = x_3;
x_11 = x_31;
goto block_30;
}
else
{
lean_inc(x_9);
lean_dec(x_3);
x_10 = lean_box(0);
x_11 = x_31;
goto block_30;
}
block_30:
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18; uint8_t x_29;
x_12 = lean_ctor_get(x_4, 0);
x_13 = lean_ctor_get(x_4, 1);
x_14 = lean_ctor_get(x_4, 2);
x_15 = lean_ctor_get(x_4, 3);
x_16 = lean_ctor_get(x_4, 4);
x_29 = !lean_is_exclusive(x_4);
if (x_29 == 0)
{
x_17 = x_4;
x_18 = x_29;
goto block_28;
}
else
{
lean_inc(x_16);
lean_inc(x_15);
lean_inc(x_14);
lean_inc(x_13);
lean_inc(x_12);
lean_dec(x_4);
x_17 = lean_box(0);
x_18 = x_29;
goto block_28;
}
block_28:
{
lean_object* x_19;
if (x_18 == 0)
{
lean_ctor_set(x_17, 3, x_13);
lean_ctor_set(x_17, 2, x_15);
lean_ctor_set(x_17, 1, x_14);
x_19 = x_17;
goto block_26;
}
else
{
lean_object* x_27;
x_27 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_27, 0, x_12);
lean_ctor_set(x_27, 1, x_14);
lean_ctor_set(x_27, 2, x_15);
lean_ctor_set(x_27, 3, x_13);
lean_ctor_set(x_27, 4, x_16);
x_19 = x_27;
goto block_26;
}
block_26:
{
lean_object* x_20;
if (x_11 == 0)
{
lean_ctor_set(x_10, 0, x_19);
x_20 = x_10;
goto block_24;
}
else
{
lean_object* x_25;
x_25 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_25, 0, x_19);
lean_ctor_set(x_25, 1, x_9);
x_20 = x_25;
goto block_24;
}
block_24:
{
lean_object* x_21;
if (x_8 == 0)
{
lean_ctor_set(x_7, 0, x_20);
x_21 = x_7;
goto block_22;
}
else
{
lean_object* x_23;
x_23 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_23, 0, x_20);
lean_ctor_set(x_23, 1, x_5);
lean_ctor_set(x_23, 2, x_6);
x_21 = x_23;
goto block_22;
}
block_22:
{
return x_21;
}
}
}
}
}
}
}
}
static lean_object* _init_l_Std_Packages_LinearPreorderOfOrdArgs_ord___autoParam(void) {
@ -16823,9 +17381,27 @@ return x_2;
LEAN_EXPORT lean_object* l_Std_LinearPreorderPackage_ofOrd(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Std_LinearPreorderPackage_ofOrd___redArg(x_2);
return x_3;
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_3 = lean_ctor_get(x_2, 0);
x_4 = lean_ctor_get(x_2, 1);
x_5 = lean_ctor_get(x_2, 2);
x_6 = lean_ctor_get(x_2, 3);
x_7 = lean_ctor_get(x_2, 4);
x_8 = lean_ctor_get(x_2, 5);
lean_inc_ref(x_7);
lean_inc_ref(x_5);
lean_inc_ref(x_8);
x_9 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_9, 0, x_4);
lean_ctor_set(x_9, 1, x_6);
lean_ctor_set(x_9, 2, x_8);
lean_ctor_set(x_9, 3, x_5);
lean_ctor_set(x_9, 4, x_7);
lean_inc_ref(x_3);
x_10 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_10, 0, x_9);
lean_ctor_set(x_10, 1, x_3);
return x_10;
}
}
LEAN_EXPORT lean_object* l_Std_LinearPreorderPackage_ofOrd___boxed(lean_object* x_1, lean_object* x_2) {
@ -18778,16 +19354,16 @@ return x_1;
LEAN_EXPORT lean_object* l_Std_LinearOrderPackage_ofOrd___redArg(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; uint8_t x_6; uint8_t x_12;
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; uint8_t x_6; uint8_t x_19;
x_2 = lean_ctor_get(x_1, 0);
x_3 = lean_ctor_get(x_1, 1);
x_4 = lean_ctor_get(x_1, 2);
x_12 = !lean_is_exclusive(x_1);
if (x_12 == 0)
x_19 = !lean_is_exclusive(x_1);
if (x_19 == 0)
{
x_5 = x_1;
x_6 = x_12;
goto block_11;
x_6 = x_19;
goto block_18;
}
else
{
@ -18796,33 +19372,53 @@ lean_inc(x_3);
lean_inc(x_2);
lean_dec(x_1);
x_5 = lean_box(0);
x_6 = x_12;
goto block_11;
x_6 = x_19;
goto block_18;
}
block_11:
block_18:
{
lean_object* x_7; lean_object* x_8;
x_7 = l_Std_LinearPreorderPackage_ofOrd___redArg(x_2);
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_7 = lean_ctor_get(x_2, 0);
lean_inc_ref(x_7);
x_8 = lean_ctor_get(x_2, 1);
lean_inc(x_8);
x_9 = lean_ctor_get(x_2, 2);
lean_inc_ref(x_9);
x_10 = lean_ctor_get(x_2, 3);
lean_inc(x_10);
x_11 = lean_ctor_get(x_2, 4);
lean_inc_ref(x_11);
x_12 = lean_ctor_get(x_2, 5);
lean_inc_ref(x_12);
lean_dec_ref(x_2);
x_13 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_13, 0, x_8);
lean_ctor_set(x_13, 1, x_10);
lean_ctor_set(x_13, 2, x_12);
lean_ctor_set(x_13, 3, x_9);
lean_ctor_set(x_13, 4, x_11);
x_14 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_14, 0, x_13);
lean_ctor_set(x_14, 1, x_7);
if (x_6 == 0)
{
lean_ctor_set(x_5, 0, x_7);
x_8 = x_5;
goto block_9;
lean_ctor_set(x_5, 0, x_14);
x_15 = x_5;
goto block_16;
}
else
{
lean_object* x_10;
x_10 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_10, 0, x_7);
lean_ctor_set(x_10, 1, x_3);
lean_ctor_set(x_10, 2, x_4);
x_8 = x_10;
goto block_9;
lean_object* x_17;
x_17 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_17, 0, x_14);
lean_ctor_set(x_17, 1, x_3);
lean_ctor_set(x_17, 2, x_4);
x_15 = x_17;
goto block_16;
}
block_9:
block_16:
{
return x_8;
return x_15;
}
}
}
@ -18830,9 +19426,73 @@ return x_8;
LEAN_EXPORT lean_object* l_Std_LinearOrderPackage_ofOrd(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Std_LinearOrderPackage_ofOrd___redArg(x_2);
return x_3;
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7; uint8_t x_20;
x_3 = lean_ctor_get(x_2, 0);
x_4 = lean_ctor_get(x_2, 1);
x_5 = lean_ctor_get(x_2, 2);
x_20 = !lean_is_exclusive(x_2);
if (x_20 == 0)
{
x_6 = x_2;
x_7 = x_20;
goto block_19;
}
else
{
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_dec(x_2);
x_6 = lean_box(0);
x_7 = x_20;
goto block_19;
}
block_19:
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
x_8 = lean_ctor_get(x_3, 0);
lean_inc_ref(x_8);
x_9 = lean_ctor_get(x_3, 1);
lean_inc(x_9);
x_10 = lean_ctor_get(x_3, 2);
lean_inc_ref(x_10);
x_11 = lean_ctor_get(x_3, 3);
lean_inc(x_11);
x_12 = lean_ctor_get(x_3, 4);
lean_inc_ref(x_12);
x_13 = lean_ctor_get(x_3, 5);
lean_inc_ref(x_13);
lean_dec_ref(x_3);
x_14 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_14, 0, x_9);
lean_ctor_set(x_14, 1, x_11);
lean_ctor_set(x_14, 2, x_13);
lean_ctor_set(x_14, 3, x_10);
lean_ctor_set(x_14, 4, x_12);
x_15 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_15, 0, x_14);
lean_ctor_set(x_15, 1, x_8);
if (x_7 == 0)
{
lean_ctor_set(x_6, 0, x_15);
x_16 = x_6;
goto block_17;
}
else
{
lean_object* x_18;
x_18 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_18, 0, x_15);
lean_ctor_set(x_18, 1, x_4);
lean_ctor_set(x_18, 2, x_5);
x_16 = x_18;
goto block_17;
}
block_17:
{
return x_16;
}
}
}
}
lean_object* runtime_initialize_Init_Data_Order_LemmasExtra(uint8_t builtin);

84
stage0/stdlib/Init/Data/String/OrderInstances.c generated
View file

@ -318,18 +318,15 @@ static lean_object* l_String_Pos_Raw_instLinearOrderPackage___closed__3;
lean_object* l_String_instDecidableLtRaw___boxed(lean_object*, lean_object*);
static const lean_closure_object l_String_Pos_Raw_instLinearOrderPackage___closed__4_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_closure_object) + sizeof(void*)*0, .m_other = 0, .m_tag = 245}, .m_fun = (void*)l_String_instDecidableLtRaw___boxed, .m_arity = 2, .m_num_fixed = 0, .m_objs = {} };
static const lean_object* l_String_Pos_Raw_instLinearOrderPackage___closed__4 = (const lean_object*)&l_String_Pos_Raw_instLinearOrderPackage___closed__4_value;
static lean_once_cell_t l_String_Pos_Raw_instLinearOrderPackage___closed__5_once = LEAN_ONCE_CELL_INITIALIZER;
static lean_object* l_String_Pos_Raw_instLinearOrderPackage___closed__5;
lean_object* l_Std_FactoryInstances_instOrdOfDecidableLE___redArg___lam__0___boxed(lean_object*, lean_object*, lean_object*);
static const lean_closure_object l_String_Pos_Raw_instLinearOrderPackage___closed__6_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_closure_object) + sizeof(void*)*1, .m_other = 0, .m_tag = 245}, .m_fun = (void*)l_Std_FactoryInstances_instOrdOfDecidableLE___redArg___lam__0___boxed, .m_arity = 3, .m_num_fixed = 1, .m_objs = {((lean_object*)&l_String_Pos_Raw_instLinearOrderPackage___closed__2_value)} };
static const lean_object* l_String_Pos_Raw_instLinearOrderPackage___closed__6 = (const lean_object*)&l_String_Pos_Raw_instLinearOrderPackage___closed__6_value;
static const lean_closure_object l_String_Pos_Raw_instLinearOrderPackage___closed__5_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_closure_object) + sizeof(void*)*1, .m_other = 0, .m_tag = 245}, .m_fun = (void*)l_Std_FactoryInstances_instOrdOfDecidableLE___redArg___lam__0___boxed, .m_arity = 3, .m_num_fixed = 1, .m_objs = {((lean_object*)&l_String_Pos_Raw_instLinearOrderPackage___closed__2_value)} };
static const lean_object* l_String_Pos_Raw_instLinearOrderPackage___closed__5 = (const lean_object*)&l_String_Pos_Raw_instLinearOrderPackage___closed__5_value;
static lean_once_cell_t l_String_Pos_Raw_instLinearOrderPackage___closed__6_once = LEAN_ONCE_CELL_INITIALIZER;
static lean_object* l_String_Pos_Raw_instLinearOrderPackage___closed__6;
static lean_once_cell_t l_String_Pos_Raw_instLinearOrderPackage___closed__7_once = LEAN_ONCE_CELL_INITIALIZER;
static lean_object* l_String_Pos_Raw_instLinearOrderPackage___closed__7;
static lean_once_cell_t l_String_Pos_Raw_instLinearOrderPackage___closed__8_once = LEAN_ONCE_CELL_INITIALIZER;
static lean_object* l_String_Pos_Raw_instLinearOrderPackage___closed__8;
lean_object* l_Std_LinearOrderPackage_ofLE___redArg(lean_object*);
static lean_once_cell_t l_String_Pos_Raw_instLinearOrderPackage___closed__9_once = LEAN_ONCE_CELL_INITIALIZER;
static lean_object* l_String_Pos_Raw_instLinearOrderPackage___closed__9;
LEAN_EXPORT lean_object* l_String_Pos_Raw_instLinearOrderPackage;
LEAN_EXPORT lean_object* l_String_Pos_instToIntCoOfNatIntHAddCastUtf8ByteSize(lean_object*);
LEAN_EXPORT lean_object* l_String_Pos_instToIntCoOfNatIntHAddCastUtf8ByteSize___boxed(lean_object*);
@ -806,14 +803,14 @@ lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_String_Pos_Raw_instLinearOrderPackage___closed__5(void) {
static lean_object* _init_l_String_Pos_Raw_instLinearOrderPackage___closed__6(void) {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = ((lean_object*)(l_String_Pos_Raw_instLinearOrderPackage___closed__4));
x_2 = lean_obj_once(&l_String_Pos_Raw_instLinearOrderPackage___closed__3, &l_String_Pos_Raw_instLinearOrderPackage___closed__3_once, _init_l_String_Pos_Raw_instLinearOrderPackage___closed__3);
x_3 = lean_box(0);
x_4 = ((lean_object*)(l_String_Pos_Raw_instLinearOrderPackage___closed__2));
x_2 = ((lean_object*)(l_String_Pos_Raw_instLinearOrderPackage___closed__2));
x_3 = lean_obj_once(&l_String_Pos_Raw_instLinearOrderPackage___closed__3, &l_String_Pos_Raw_instLinearOrderPackage___closed__3_once, _init_l_String_Pos_Raw_instLinearOrderPackage___closed__3);
x_4 = lean_box(0);
x_5 = lean_box(0);
x_6 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_6, 0, x_5);
@ -828,8 +825,8 @@ static lean_object* _init_l_String_Pos_Raw_instLinearOrderPackage___closed__7(vo
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = ((lean_object*)(l_String_Pos_Raw_instLinearOrderPackage___closed__6));
x_2 = lean_obj_once(&l_String_Pos_Raw_instLinearOrderPackage___closed__5, &l_String_Pos_Raw_instLinearOrderPackage___closed__5_once, _init_l_String_Pos_Raw_instLinearOrderPackage___closed__5);
x_1 = ((lean_object*)(l_String_Pos_Raw_instLinearOrderPackage___closed__5));
x_2 = lean_obj_once(&l_String_Pos_Raw_instLinearOrderPackage___closed__6, &l_String_Pos_Raw_instLinearOrderPackage___closed__6_once, _init_l_String_Pos_Raw_instLinearOrderPackage___closed__6);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
@ -850,20 +847,11 @@ lean_ctor_set(x_4, 2, x_1);
return x_4;
}
}
static lean_object* _init_l_String_Pos_Raw_instLinearOrderPackage___closed__9(void) {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_obj_once(&l_String_Pos_Raw_instLinearOrderPackage___closed__8, &l_String_Pos_Raw_instLinearOrderPackage___closed__8_once, _init_l_String_Pos_Raw_instLinearOrderPackage___closed__8);
x_2 = l_Std_LinearOrderPackage_ofLE___redArg(x_1);
return x_2;
}
}
static lean_object* _init_l_String_Pos_Raw_instLinearOrderPackage(void) {
_start:
{
lean_object* x_1;
x_1 = lean_obj_once(&l_String_Pos_Raw_instLinearOrderPackage___closed__9, &l_String_Pos_Raw_instLinearOrderPackage___closed__9_once, _init_l_String_Pos_Raw_instLinearOrderPackage___closed__9);
x_1 = lean_obj_once(&l_String_Pos_Raw_instLinearOrderPackage___closed__8, &l_String_Pos_Raw_instLinearOrderPackage___closed__8_once, _init_l_String_Pos_Raw_instLinearOrderPackage___closed__8);
return x_1;
}
}
@ -902,7 +890,7 @@ return x_2;
LEAN_EXPORT lean_object* l_String_Pos_instLinearOrderPackage(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_2 = ((lean_object*)(l_String_Pos_Raw_instLinearOrderPackage___closed__0));
x_3 = ((lean_object*)(l_String_Pos_Raw_instLinearOrderPackage___closed__1));
x_4 = lean_box(0);
@ -918,23 +906,22 @@ lean_closure_set(x_8, 0, x_7);
x_9 = lean_alloc_closure((void*)(l_String_instDecidableLtPos___boxed), 3, 1);
lean_closure_set(x_9, 0, x_1);
lean_inc_ref(x_5);
x_10 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_10, 0, x_4);
lean_ctor_set(x_10, 1, x_5);
lean_ctor_set(x_10, 2, x_6);
lean_ctor_set(x_10, 3, x_8);
lean_ctor_set(x_10, 4, x_9);
x_11 = lean_alloc_closure((void*)(l_Std_FactoryInstances_instOrdOfDecidableLE___redArg___lam__0___boxed), 3, 1);
lean_closure_set(x_11, 0, x_5);
x_10 = lean_alloc_closure((void*)(l_Std_FactoryInstances_instOrdOfDecidableLE___redArg___lam__0___boxed), 3, 1);
lean_closure_set(x_10, 0, x_5);
x_11 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_11, 0, x_4);
lean_ctor_set(x_11, 1, x_6);
lean_ctor_set(x_11, 2, x_8);
lean_ctor_set(x_11, 3, x_5);
lean_ctor_set(x_11, 4, x_9);
x_12 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_12, 0, x_10);
lean_ctor_set(x_12, 1, x_11);
lean_ctor_set(x_12, 0, x_11);
lean_ctor_set(x_12, 1, x_10);
x_13 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_13, 0, x_12);
lean_ctor_set(x_13, 1, x_2);
lean_ctor_set(x_13, 2, x_3);
x_14 = l_Std_LinearOrderPackage_ofLE___redArg(x_13);
return x_14;
return x_13;
}
}
LEAN_EXPORT lean_object* l_String_Slice_Pos_instToIntCoOfNatIntHAddCastUtf8ByteSize(lean_object* x_1) {
@ -972,7 +959,7 @@ return x_2;
LEAN_EXPORT lean_object* l_String_Slice_Pos_instLinearOrderPackage(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_2 = ((lean_object*)(l_String_Pos_Raw_instLinearOrderPackage___closed__0));
x_3 = ((lean_object*)(l_String_Pos_Raw_instLinearOrderPackage___closed__1));
x_4 = lean_box(0);
@ -988,23 +975,22 @@ lean_closure_set(x_8, 0, x_7);
x_9 = lean_alloc_closure((void*)(l_String_instDecidableLtPos__1___boxed), 3, 1);
lean_closure_set(x_9, 0, x_1);
lean_inc_ref(x_5);
x_10 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_10, 0, x_4);
lean_ctor_set(x_10, 1, x_5);
lean_ctor_set(x_10, 2, x_6);
lean_ctor_set(x_10, 3, x_8);
lean_ctor_set(x_10, 4, x_9);
x_11 = lean_alloc_closure((void*)(l_Std_FactoryInstances_instOrdOfDecidableLE___redArg___lam__0___boxed), 3, 1);
lean_closure_set(x_11, 0, x_5);
x_10 = lean_alloc_closure((void*)(l_Std_FactoryInstances_instOrdOfDecidableLE___redArg___lam__0___boxed), 3, 1);
lean_closure_set(x_10, 0, x_5);
x_11 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_11, 0, x_4);
lean_ctor_set(x_11, 1, x_6);
lean_ctor_set(x_11, 2, x_8);
lean_ctor_set(x_11, 3, x_5);
lean_ctor_set(x_11, 4, x_9);
x_12 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_12, 0, x_10);
lean_ctor_set(x_12, 1, x_11);
lean_ctor_set(x_12, 0, x_11);
lean_ctor_set(x_12, 1, x_10);
x_13 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_13, 0, x_12);
lean_ctor_set(x_13, 1, x_2);
lean_ctor_set(x_13, 2, x_3);
x_14 = l_Std_LinearOrderPackage_ofLE___redArg(x_13);
return x_14;
return x_13;
}
}
lean_object* runtime_initialize_Init_Data_String_Defs(uint8_t builtin);

12
stage0/stdlib/Lean/Compiler.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Compiler
// Imports: public import Lean.Compiler.InlineAttrs public import Lean.Compiler.Specialize public import Lean.Compiler.ClosedTermCache public import Lean.Compiler.ExternAttr public import Lean.Compiler.ImplementedByAttr public import Lean.Compiler.NeverExtractAttr public import Lean.Compiler.IR public import Lean.Compiler.CSimpAttr public import Lean.Compiler.FFI public import Lean.Compiler.MetaAttr public import Lean.Compiler.NoncomputableAttr public import Lean.Compiler.Main public import Lean.Compiler.Old
// Imports: public import Lean.Compiler.InlineAttrs public import Lean.Compiler.Specialize public import Lean.Compiler.ClosedTermCache public import Lean.Compiler.ExternAttr public import Lean.Compiler.ImplementedByAttr public import Lean.Compiler.NeverExtractAttr public import Lean.Compiler.IR public import Lean.Compiler.CSimpAttr public import Lean.Compiler.FFI public import Lean.Compiler.MetaAttr public import Lean.Compiler.NoncomputableAttr public import Lean.Compiler.Main public import Lean.Compiler.NameDemangling public import Lean.Compiler.Old
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -25,6 +25,7 @@ lean_object* runtime_initialize_Lean_Compiler_FFI(uint8_t builtin);
lean_object* runtime_initialize_Lean_Compiler_MetaAttr(uint8_t builtin);
lean_object* runtime_initialize_Lean_Compiler_NoncomputableAttr(uint8_t builtin);
lean_object* runtime_initialize_Lean_Compiler_Main(uint8_t builtin);
lean_object* runtime_initialize_Lean_Compiler_NameDemangling(uint8_t builtin);
lean_object* runtime_initialize_Lean_Compiler_Old(uint8_t builtin);
static bool _G_runtime_initialized = false;
LEAN_EXPORT lean_object* runtime_initialize_Lean_Compiler(uint8_t builtin) {
@ -79,6 +80,10 @@ res = runtime_initialize_Lean_Compiler_Main(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Lean_Compiler_NameDemangling(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Lean_Compiler_Old(builtin)
;
if (lean_io_result_is_error(res)) return res;
@ -104,6 +109,7 @@ lean_object* initialize_Lean_Compiler_FFI(uint8_t builtin);
lean_object* initialize_Lean_Compiler_MetaAttr(uint8_t builtin);
lean_object* initialize_Lean_Compiler_NoncomputableAttr(uint8_t builtin);
lean_object* initialize_Lean_Compiler_Main(uint8_t builtin);
lean_object* initialize_Lean_Compiler_NameDemangling(uint8_t builtin);
lean_object* initialize_Lean_Compiler_Old(uint8_t builtin);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Lean_Compiler(uint8_t builtin) {
@ -158,6 +164,10 @@ res = initialize_Lean_Compiler_Main(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Compiler_NameDemangling(builtin)
;
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Compiler_Old(builtin)
;
if (lean_io_result_is_error(res)) return res;

245
stage0/stdlib/Lean/Compiler/LCNF/Simp/ConstantFold.c generated
View file

@ -93,8 +93,6 @@ LEAN_EXPORT lean_object* l___private_Lean_Compiler_LCNF_Simp_ConstantFold_0__Lea
LEAN_EXPORT lean_object* l___private_Lean_Compiler_LCNF_Simp_ConstantFold_0__Lean_Compiler_LCNF_Simp_ConstantFold_getLitAux___redArg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Compiler_LCNF_Simp_ConstantFold_0__Lean_Compiler_LCNF_Simp_ConstantFold_getLitAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Compiler_LCNF_Simp_ConstantFold_0__Lean_Compiler_LCNF_Simp_ConstantFold_getLitAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_mkAuxLit___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance_spec__0(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_mkAuxLit___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance_spec__0___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance___redArg___lam__0(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance___redArg___lam__0___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static const lean_string_object l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance___redArg___lam__1___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 = "_x"};
@ -102,8 +100,8 @@ static const lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperIns
lean_object* l_Lean_Name_mkStr1(lean_object*);
static const lean_ctor_object l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance___redArg___lam__1___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_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance___redArg___lam__1___closed__0_value),LEAN_SCALAR_PTR_LITERAL(181, 1, 28, 251, 11, 9, 217, 106)}};
static const lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance___redArg___lam__1___closed__1 = (const lean_object*)&l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance___redArg___lam__1___closed__1_value;
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance___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_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance___redArg___lam__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance___redArg___lam__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance___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_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance___redArg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Char_ofNat___boxed(lean_object*);
@ -189,21 +187,23 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_getPseudoListLit
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_getPseudoListLiteral___redArg___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_getPseudoListLiteral(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_getPseudoListLiteral___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static const lean_string_object l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0___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 = "Array"};
static const lean_object* l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0___closed__0 = (const lean_object*)&l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0___closed__0_value;
static const lean_string_object l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0___closed__1_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 = "push"};
static const lean_object* l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0___closed__1 = (const lean_object*)&l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0___closed__1_value;
static const lean_ctor_object l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0___closed__2_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___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0___closed__0_value),LEAN_SCALAR_PTR_LITERAL(81, 46, 193, 1, 46, 43, 107, 121)}};
static const lean_ctor_object l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0___closed__2_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___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0___closed__2_value_aux_0),((lean_object*)&l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0___closed__1_value),LEAN_SCALAR_PTR_LITERAL(72, 153, 248, 33, 206, 118, 72, 33)}};
static const lean_object* l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0___closed__2 = (const lean_object*)&l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0___closed__2_value;
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_mkAuxLit___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_mkAuxLit___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static const lean_string_object l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__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 = "Array"};
static const lean_object* l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__1___closed__0 = (const lean_object*)&l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__1___closed__0_value;
static const lean_string_object l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__1___closed__1_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 = "push"};
static const lean_object* l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__1___closed__1 = (const lean_object*)&l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__1___closed__1_value;
static const lean_ctor_object l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__1___closed__2_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___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__1___closed__0_value),LEAN_SCALAR_PTR_LITERAL(81, 46, 193, 1, 46, 43, 107, 121)}};
static const lean_ctor_object l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__1___closed__2_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___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__1___closed__2_value_aux_0),((lean_object*)&l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__1___closed__1_value),LEAN_SCALAR_PTR_LITERAL(72, 153, 248, 33, 206, 118, 72, 33)}};
static const lean_object* l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__1___closed__2 = (const lean_object*)&l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__1___closed__2_value;
uint8_t lean_usize_dec_lt(size_t, size_t);
lean_object* lean_array_uget_borrowed(lean_object*, size_t);
size_t lean_usize_add(size_t, size_t);
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0___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_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__1(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__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*);
static const lean_string_object l_Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 8, .m_capacity = 8, .m_length = 7, .m_data = "mkEmpty"};
static const lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral___closed__0 = (const lean_object*)&l_Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral___closed__0_value;
static const lean_ctor_object l_Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral___closed__1_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___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0___closed__0_value),LEAN_SCALAR_PTR_LITERAL(81, 46, 193, 1, 46, 43, 107, 121)}};
static const lean_ctor_object l_Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral___closed__1_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___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__1___closed__0_value),LEAN_SCALAR_PTR_LITERAL(81, 46, 193, 1, 46, 43, 107, 121)}};
static const lean_ctor_object l_Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral___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*)&l_Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral___closed__1_value_aux_0),((lean_object*)&l_Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral___closed__0_value),LEAN_SCALAR_PTR_LITERAL(242, 217, 122, 134, 168, 122, 153, 10)}};
static const lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral___closed__1 = (const lean_object*)&l_Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral___closed__1_value;
size_t lean_array_size(lean_object*);
@ -1703,7 +1703,7 @@ static const lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_stringFolders__
static const lean_ctor_object l_Lean_Compiler_LCNF_Simp_ConstantFold_stringFolders___closed__13_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)&l_Lean_Compiler_LCNF_Simp_ConstantFold_stringFolders___closed__10_value),((lean_object*)&l_Lean_Compiler_LCNF_Simp_ConstantFold_stringFolders___closed__12_value)}};
static const lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_stringFolders___closed__13 = (const lean_object*)&l_Lean_Compiler_LCNF_Simp_ConstantFold_stringFolders___closed__13_value;
static const lean_ctor_object l_Lean_Compiler_LCNF_Simp_ConstantFold_stringFolders___closed__14_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_Compiler_LCNF_Simp_ConstantFold_relationFolders___closed__52_value),LEAN_SCALAR_PTR_LITERAL(6, 130, 56, 8, 41, 104, 134, 43)}};
static const lean_ctor_object l_Lean_Compiler_LCNF_Simp_ConstantFold_stringFolders___closed__14_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_Compiler_LCNF_Simp_ConstantFold_stringFolders___closed__14_value_aux_0),((lean_object*)&l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0___closed__1_value),LEAN_SCALAR_PTR_LITERAL(235, 214, 172, 180, 192, 17, 133, 66)}};
static const lean_ctor_object l_Lean_Compiler_LCNF_Simp_ConstantFold_stringFolders___closed__14_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_Compiler_LCNF_Simp_ConstantFold_stringFolders___closed__14_value_aux_0),((lean_object*)&l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__1___closed__1_value),LEAN_SCALAR_PTR_LITERAL(235, 214, 172, 180, 192, 17, 133, 66)}};
static const lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_stringFolders___closed__14 = (const lean_object*)&l_Lean_Compiler_LCNF_Simp_ConstantFold_stringFolders___closed__14_value;
lean_object* l_String_push___boxed(lean_object*, lean_object*);
static const lean_closure_object l_Lean_Compiler_LCNF_Simp_ConstantFold_stringFolders___closed__15_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_closure_object) + sizeof(void*)*0, .m_other = 0, .m_tag = 245}, .m_fun = (void*)l_String_push___boxed, .m_arity = 2, .m_num_fixed = 0, .m_objs = {} };
@ -3476,27 +3476,6 @@ lean_dec(x_2);
return x_10;
}
}
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_mkAuxLit___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance_spec__0(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_9 = l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatLit___redArg(x_1);
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
lean_dec_ref(x_9);
x_11 = l_Lean_Compiler_LCNF_Simp_ConstantFold_mkAuxLetDecl(x_10, x_2, x_3, x_4, x_5, x_6, x_7);
return x_11;
}
}
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_mkAuxLit___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance_spec__0___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
lean_object* x_9;
x_9 = l_Lean_Compiler_LCNF_Simp_ConstantFold_mkAuxLit___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance_spec__0(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
lean_dec(x_3);
return x_9;
}
}
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance___redArg___lam__0(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
@ -3519,133 +3498,134 @@ lean_dec(x_2);
return x_9;
}
}
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance___redArg___lam__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance___redArg___lam__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
_start:
{
lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_10 = lean_apply_1(x_1, x_3);
x_11 = ((lean_object*)(l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance___redArg___lam__1___closed__1));
x_12 = l_Lean_Compiler_LCNF_Simp_ConstantFold_mkAuxLit___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance_spec__0(x_10, x_11, x_4, x_5, x_6, x_7, x_8);
if (lean_obj_tag(x_12) == 0)
lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_11 = lean_apply_1(x_1, x_4);
x_12 = ((lean_object*)(l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance___redArg___lam__1___closed__1));
x_13 = l_Lean_Compiler_LCNF_Simp_ConstantFold_mkAuxLit___redArg(x_2, x_11, x_12, x_5, x_6, x_7, x_8, x_9);
if (lean_obj_tag(x_13) == 0)
{
lean_object* x_13; lean_object* x_14; uint8_t x_15; uint8_t x_26;
x_13 = lean_ctor_get(x_12, 0);
x_26 = !lean_is_exclusive(x_12);
if (x_26 == 0)
lean_object* x_14; lean_object* x_15; uint8_t x_16; uint8_t x_27;
x_14 = lean_ctor_get(x_13, 0);
x_27 = !lean_is_exclusive(x_13);
if (x_27 == 0)
{
x_14 = x_12;
x_15 = x_26;
goto block_25;
x_15 = x_13;
x_16 = x_27;
goto block_26;
}
else
{
lean_inc(x_13);
lean_dec(x_12);
x_14 = lean_box(0);
x_15 = x_26;
goto block_25;
lean_inc(x_14);
lean_dec(x_13);
x_15 = lean_box(0);
x_16 = x_27;
goto block_26;
}
block_25:
block_26:
{
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_16 = lean_box(0);
x_17 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_17, 0, x_13);
x_18 = lean_unsigned_to_nat(1u);
x_19 = lean_mk_empty_array_with_capacity(x_18);
x_20 = lean_array_push(x_19, x_17);
x_21 = lean_alloc_ctor(3, 3, 0);
lean_ctor_set(x_21, 0, x_2);
lean_ctor_set(x_21, 1, x_16);
lean_ctor_set(x_21, 2, x_20);
if (x_15 == 0)
lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_17 = lean_box(0);
x_18 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_18, 0, x_14);
x_19 = lean_unsigned_to_nat(1u);
x_20 = lean_mk_empty_array_with_capacity(x_19);
x_21 = lean_array_push(x_20, x_18);
x_22 = lean_alloc_ctor(3, 3, 0);
lean_ctor_set(x_22, 0, x_3);
lean_ctor_set(x_22, 1, x_17);
lean_ctor_set(x_22, 2, x_21);
if (x_16 == 0)
{
lean_ctor_set(x_14, 0, x_21);
x_22 = x_14;
goto block_23;
lean_ctor_set(x_15, 0, x_22);
x_23 = x_15;
goto block_24;
}
else
{
lean_object* x_24;
x_24 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_24, 0, x_21);
x_22 = x_24;
goto block_23;
lean_object* x_25;
x_25 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_25, 0, x_22);
x_23 = x_25;
goto block_24;
}
block_23:
block_24:
{
return x_22;
return x_23;
}
}
}
else
{
lean_object* x_27; lean_object* x_28; uint8_t x_29; uint8_t x_34;
lean_dec(x_2);
x_27 = lean_ctor_get(x_12, 0);
x_34 = !lean_is_exclusive(x_12);
if (x_34 == 0)
lean_object* x_28; lean_object* x_29; uint8_t x_30; uint8_t x_35;
lean_dec(x_3);
x_28 = lean_ctor_get(x_13, 0);
x_35 = !lean_is_exclusive(x_13);
if (x_35 == 0)
{
x_28 = x_12;
x_29 = x_34;
goto block_33;
x_29 = x_13;
x_30 = x_35;
goto block_34;
}
else
{
lean_inc(x_27);
lean_dec(x_12);
x_28 = lean_box(0);
x_29 = x_34;
goto block_33;
lean_inc(x_28);
lean_dec(x_13);
x_29 = lean_box(0);
x_30 = x_35;
goto block_34;
}
block_33:
block_34:
{
lean_object* x_30;
if (x_29 == 0)
lean_object* x_31;
if (x_30 == 0)
{
x_30 = x_28;
goto block_31;
x_31 = x_29;
goto block_32;
}
else
{
lean_object* x_32;
x_32 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_32, 0, x_27);
x_30 = x_32;
goto block_31;
lean_object* x_33;
x_33 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_33, 0, x_28);
x_31 = x_33;
goto block_32;
}
block_31:
block_32:
{
return x_30;
return x_31;
}
}
}
}
}
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance___redArg___lam__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance___redArg___lam__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_10;
x_10 = l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance___redArg___lam__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
lean_dec(x_4);
return x_10;
lean_object* x_11;
x_11 = l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance___redArg___lam__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
return x_11;
}
}
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance___redArg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6;
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
lean_inc(x_2);
x_4 = lean_alloc_closure((void*)(l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance___redArg___lam__0___boxed), 8, 2);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
x_5 = lean_alloc_closure((void*)(l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance___redArg___lam__1___boxed), 9, 2);
lean_closure_set(x_5, 0, x_3);
lean_closure_set(x_5, 1, x_2);
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_4);
lean_ctor_set(x_6, 1, x_5);
return x_6;
x_5 = ((lean_object*)(l_Lean_Compiler_LCNF_Simp_ConstantFold_instLiteralNat));
x_6 = lean_alloc_closure((void*)(l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance___redArg___lam__1___boxed), 10, 3);
lean_closure_set(x_6, 0, x_3);
lean_closure_set(x_6, 1, x_5);
lean_closure_set(x_6, 2, x_2);
x_7 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_7, 0, x_4);
lean_ctor_set(x_7, 1, x_6);
return x_7;
}
}
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
@ -4663,7 +4643,28 @@ lean_dec_ref(x_2);
return x_7;
}
}
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0(lean_object* x_1, lean_object* x_2, lean_object* x_3, size_t x_4, size_t x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_mkAuxLit___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_9 = l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatLit___redArg(x_1);
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
lean_dec_ref(x_9);
x_11 = l_Lean_Compiler_LCNF_Simp_ConstantFold_mkAuxLetDecl(x_10, x_2, x_3, x_4, x_5, x_6, x_7);
return x_11;
}
}
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_mkAuxLit___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
lean_object* x_9;
x_9 = l_Lean_Compiler_LCNF_Simp_ConstantFold_mkAuxLit___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
lean_dec(x_3);
return x_9;
}
}
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, size_t x_4, size_t x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
_start:
{
uint8_t x_13;
@ -4686,7 +4687,7 @@ else
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_15 = ((lean_object*)(l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance___redArg___lam__1___closed__1));
x_16 = lean_array_uget_borrowed(x_3, x_5);
x_17 = ((lean_object*)(l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0___closed__2));
x_17 = ((lean_object*)(l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__1___closed__2));
x_18 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_18, 0, x_6);
lean_inc(x_16);
@ -4733,7 +4734,7 @@ return x_26;
}
}
}
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12) {
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12) {
_start:
{
size_t x_13; size_t x_14; lean_object* x_15;
@ -4741,7 +4742,7 @@ x_13 = lean_unbox_usize(x_4);
lean_dec(x_4);
x_14 = lean_unbox_usize(x_5);
lean_dec(x_5);
x_15 = l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0(x_1, x_2, x_3, x_13, x_14, x_6, x_7, x_8, x_9, x_10, x_11);
x_15 = l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__1(x_1, x_2, x_3, x_13, x_14, x_6, x_7, x_8, x_9, x_10, x_11);
lean_dec(x_7);
lean_dec_ref(x_3);
return x_15;
@ -4757,7 +4758,7 @@ lean_inc(x_8);
lean_inc_ref(x_7);
lean_inc(x_6);
lean_inc_ref(x_5);
x_12 = l_Lean_Compiler_LCNF_Simp_ConstantFold_mkAuxLit___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance_spec__0(x_10, x_11, x_4, x_5, x_6, x_7, x_8);
x_12 = l_Lean_Compiler_LCNF_Simp_ConstantFold_mkAuxLit___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0(x_10, x_11, x_4, x_5, x_6, x_7, x_8);
if (lean_obj_tag(x_12) == 0)
{
lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24;
@ -4796,7 +4797,7 @@ lean_inc(x_25);
lean_dec_ref(x_24);
x_26 = lean_array_size(x_1);
x_27 = 0;
x_28 = l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0(x_17, x_16, x_1, x_26, x_27, x_25, x_4, x_5, x_6, x_7, x_8);
x_28 = l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__1(x_17, x_16, x_1, x_26, x_27, x_25, x_4, x_5, x_6, x_7, x_8);
if (lean_obj_tag(x_28) == 0)
{
lean_object* x_29; lean_object* x_30; uint8_t x_31; uint8_t x_38;
@ -24667,7 +24668,7 @@ else
lean_object* x_42; lean_object* x_43;
lean_del_object(x_30);
x_42 = ((lean_object*)(l_Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance___redArg___lam__1___closed__1));
x_43 = l_Lean_Compiler_LCNF_Simp_ConstantFold_mkAuxLit___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkNatWrapperInstance_spec__0(x_35, x_42, x_5, x_6, x_7, x_8, x_9);
x_43 = l_Lean_Compiler_LCNF_Simp_ConstantFold_mkAuxLit___at___00Lean_Compiler_LCNF_Simp_ConstantFold_mkPseudoArrayLiteral_spec__0(x_35, x_42, x_5, x_6, x_7, x_8, x_9);
if (lean_obj_tag(x_43) == 0)
{
lean_object* x_44; lean_object* x_45; uint8_t x_46; uint8_t x_64;

6452
stage0/stdlib/Lean/Compiler/NameDemangling.c generated Normal file
View file

File diff suppressed because it is too large Load diff

81
stage0/stdlib/Lean/Data/NameTrie.c generated
View file

@ -22,15 +22,26 @@ LEAN_EXPORT lean_object* l_Lean_NamePart_str_elim___redArg(lean_object*, lean_ob
LEAN_EXPORT lean_object* l_Lean_NamePart_str_elim(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_NamePart_num_elim___redArg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_NamePart_num_elim(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_string_dec_eq(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Lean_instBEqNamePart_beq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_instBEqNamePart_beq___boxed(lean_object*, lean_object*);
static const lean_closure_object l_Lean_instBEqNamePart___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_closure_object) + sizeof(void*)*0, .m_other = 0, .m_tag = 245}, .m_fun = (void*)l_Lean_instBEqNamePart_beq___boxed, .m_arity = 2, .m_num_fixed = 0, .m_objs = {} };
static const lean_object* l_Lean_instBEqNamePart___closed__0 = (const lean_object*)&l_Lean_instBEqNamePart___closed__0_value;
LEAN_EXPORT const lean_object* l_Lean_instBEqNamePart = (const lean_object*)&l_Lean_instBEqNamePart___closed__0_value;
static const lean_string_object l_Lean_instInhabitedNamePart_default___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 1, .m_capacity = 1, .m_length = 0, .m_data = ""};
static const lean_object* l_Lean_instInhabitedNamePart_default___closed__0 = (const lean_object*)&l_Lean_instInhabitedNamePart_default___closed__0_value;
static const lean_ctor_object l_Lean_instInhabitedNamePart_default___closed__1_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*1 + 0, .m_other = 1, .m_tag = 0}, .m_objs = {((lean_object*)&l_Lean_instInhabitedNamePart_default___closed__0_value)}};
static const lean_object* l_Lean_instInhabitedNamePart_default___closed__1 = (const lean_object*)&l_Lean_instInhabitedNamePart_default___closed__1_value;
LEAN_EXPORT const lean_object* l_Lean_instInhabitedNamePart_default = (const lean_object*)&l_Lean_instInhabitedNamePart_default___closed__1_value;
LEAN_EXPORT const lean_object* l_Lean_instInhabitedNamePart = (const lean_object*)&l_Lean_instInhabitedNamePart_default___closed__1_value;
lean_object* l_Nat_reprFast(lean_object*);
LEAN_EXPORT lean_object* l_Lean_instToStringNamePart___lam__0(lean_object*);
static const lean_closure_object l_Lean_instToStringNamePart___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_closure_object) + sizeof(void*)*0, .m_other = 0, .m_tag = 245}, .m_fun = (void*)l_Lean_instToStringNamePart___lam__0, .m_arity = 1, .m_num_fixed = 0, .m_objs = {} };
static const lean_object* l_Lean_instToStringNamePart___closed__0 = (const lean_object*)&l_Lean_instToStringNamePart___closed__0_value;
LEAN_EXPORT const lean_object* l_Lean_instToStringNamePart = (const lean_object*)&l_Lean_instToStringNamePart___closed__0_value;
uint8_t lean_string_dec_lt(lean_object*, lean_object*);
uint8_t lean_string_dec_eq(lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Lean_NamePart_cmp(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_NamePart_cmp___boxed(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Lean_NamePart_lt(lean_object*, lean_object*);
@ -232,6 +243,56 @@ x_5 = l_Lean_NamePart_ctorElim___redArg(x_2, x_4);
return x_5;
}
}
LEAN_EXPORT uint8_t l_Lean_instBEqNamePart_beq(lean_object* x_1, lean_object* x_2) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_3; lean_object* x_4; uint8_t x_5;
x_3 = lean_ctor_get(x_1, 0);
x_4 = lean_ctor_get(x_2, 0);
x_5 = lean_string_dec_eq(x_3, x_4);
return x_5;
}
else
{
uint8_t x_6;
x_6 = 0;
return x_6;
}
}
else
{
if (lean_obj_tag(x_2) == 1)
{
lean_object* x_7; lean_object* x_8; uint8_t x_9;
x_7 = lean_ctor_get(x_1, 0);
x_8 = lean_ctor_get(x_2, 0);
x_9 = lean_nat_dec_eq(x_7, x_8);
return x_9;
}
else
{
uint8_t x_10;
x_10 = 0;
return x_10;
}
}
}
}
LEAN_EXPORT lean_object* l_Lean_instBEqNamePart_beq___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l_Lean_instBEqNamePart_beq(x_1, x_2);
lean_dec_ref(x_2);
lean_dec_ref(x_1);
x_4 = lean_box(x_3);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Lean_instToStringNamePart___lam__0(lean_object* x_1) {
_start:
{
@ -777,9 +838,9 @@ goto block_64;
block_54:
{
lean_object* x_47; lean_object* x_48;
x_47 = lean_nat_add(x_44, x_46);
x_47 = lean_nat_add(x_45, x_46);
lean_dec(x_46);
lean_dec(x_44);
lean_dec(x_45);
if (x_40 == 0)
{
lean_ctor_set(x_39, 4, x_8);
@ -808,7 +869,7 @@ lean_object* x_49;
if (x_29 == 0)
{
lean_ctor_set(x_28, 4, x_48);
lean_ctor_set(x_28, 3, x_45);
lean_ctor_set(x_28, 3, x_44);
lean_ctor_set(x_28, 2, x_33);
lean_ctor_set(x_28, 1, x_32);
lean_ctor_set(x_28, 0, x_43);
@ -822,7 +883,7 @@ x_51 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_51, 0, x_43);
lean_ctor_set(x_51, 1, x_32);
lean_ctor_set(x_51, 2, x_33);
lean_ctor_set(x_51, 3, x_45);
lean_ctor_set(x_51, 3, x_44);
lean_ctor_set(x_51, 4, x_48);
x_49 = x_51;
goto block_50;
@ -870,8 +931,8 @@ if (lean_obj_tag(x_35) == 0)
lean_object* x_60;
x_60 = lean_ctor_get(x_35, 0);
lean_inc(x_60);
x_44 = x_59;
x_45 = x_58;
x_44 = x_58;
x_45 = x_59;
x_46 = x_60;
goto block_54;
}
@ -879,8 +940,8 @@ else
{
lean_object* x_61;
x_61 = lean_unsigned_to_nat(0u);
x_44 = x_59;
x_45 = x_58;
x_44 = x_58;
x_45 = x_59;
x_46 = x_61;
goto block_54;
}

3646
stage0/stdlib/Lean/Elab/Deriving/TypeName.c generated
View file

File diff suppressed because it is too large Load diff

307
stage0/stdlib/Lean/Elab/DocString/Builtin.c generated
View file

@ -2538,9 +2538,9 @@ static const lean_string_object l_Lean_Doc_output___regBuiltin_Lean_Doc_output_g
static const lean_object* l_Lean_Doc_output___regBuiltin_Lean_Doc_output_getArgs_docString__5___closed__0 = (const lean_object*)&l_Lean_Doc_output___regBuiltin_Lean_Doc_output_getArgs_docString__5___closed__0_value;
LEAN_EXPORT lean_object* l_Lean_Doc_output___regBuiltin_Lean_Doc_output_getArgs_docString__5();
LEAN_EXPORT lean_object* l_Lean_Doc_output___regBuiltin_Lean_Doc_output_getArgs_docString__5___boxed(lean_object*);
static const lean_ctor_object l_Lean_Doc_output___regBuiltin_Lean_Doc_output_getArgs_declRange__7___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1003) << 1) | 1)),((lean_object*)(((size_t)(2) << 1) | 1))}};
static const lean_ctor_object l_Lean_Doc_output___regBuiltin_Lean_Doc_output_getArgs_declRange__7___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1007) << 1) | 1)),((lean_object*)(((size_t)(2) << 1) | 1))}};
static const lean_object* l_Lean_Doc_output___regBuiltin_Lean_Doc_output_getArgs_declRange__7___closed__0 = (const lean_object*)&l_Lean_Doc_output___regBuiltin_Lean_Doc_output_getArgs_declRange__7___closed__0_value;
static const lean_ctor_object l_Lean_Doc_output___regBuiltin_Lean_Doc_output_getArgs_declRange__7___closed__1_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1003) << 1) | 1)),((lean_object*)(((size_t)(24) << 1) | 1))}};
static const lean_ctor_object l_Lean_Doc_output___regBuiltin_Lean_Doc_output_getArgs_declRange__7___closed__1_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1007) << 1) | 1)),((lean_object*)(((size_t)(24) << 1) | 1))}};
static const lean_object* l_Lean_Doc_output___regBuiltin_Lean_Doc_output_getArgs_declRange__7___closed__1 = (const lean_object*)&l_Lean_Doc_output___regBuiltin_Lean_Doc_output_getArgs_declRange__7___closed__1_value;
static const lean_ctor_object l_Lean_Doc_output___regBuiltin_Lean_Doc_output_getArgs_declRange__7___closed__2_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*4 + 0, .m_other = 4, .m_tag = 0}, .m_objs = {((lean_object*)&l_Lean_Doc_output___regBuiltin_Lean_Doc_output_getArgs_declRange__7___closed__0_value),((lean_object*)(((size_t)(2) << 1) | 1)),((lean_object*)&l_Lean_Doc_output___regBuiltin_Lean_Doc_output_getArgs_declRange__7___closed__1_value),((lean_object*)(((size_t)(24) << 1) | 1))}};
static const lean_object* l_Lean_Doc_output___regBuiltin_Lean_Doc_output_getArgs_declRange__7___closed__2 = (const lean_object*)&l_Lean_Doc_output___regBuiltin_Lean_Doc_output_getArgs_declRange__7___closed__2_value;
@ -2571,9 +2571,9 @@ static const lean_string_object l_Lean_Doc_lit___regBuiltin_Lean_Doc_lit_getArgs
static const lean_object* l_Lean_Doc_lit___regBuiltin_Lean_Doc_lit_getArgs_docString__5___closed__0 = (const lean_object*)&l_Lean_Doc_lit___regBuiltin_Lean_Doc_lit_getArgs_docString__5___closed__0_value;
LEAN_EXPORT lean_object* l_Lean_Doc_lit___regBuiltin_Lean_Doc_lit_getArgs_docString__5();
LEAN_EXPORT lean_object* l_Lean_Doc_lit___regBuiltin_Lean_Doc_lit_getArgs_docString__5___boxed(lean_object*);
static const lean_ctor_object l_Lean_Doc_lit___regBuiltin_Lean_Doc_lit_getArgs_declRange__7___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1046) << 1) | 1)),((lean_object*)(((size_t)(2) << 1) | 1))}};
static const lean_ctor_object l_Lean_Doc_lit___regBuiltin_Lean_Doc_lit_getArgs_declRange__7___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1050) << 1) | 1)),((lean_object*)(((size_t)(2) << 1) | 1))}};
static const lean_object* l_Lean_Doc_lit___regBuiltin_Lean_Doc_lit_getArgs_declRange__7___closed__0 = (const lean_object*)&l_Lean_Doc_lit___regBuiltin_Lean_Doc_lit_getArgs_declRange__7___closed__0_value;
static const lean_ctor_object l_Lean_Doc_lit___regBuiltin_Lean_Doc_lit_getArgs_declRange__7___closed__1_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1046) << 1) | 1)),((lean_object*)(((size_t)(18) << 1) | 1))}};
static const lean_ctor_object l_Lean_Doc_lit___regBuiltin_Lean_Doc_lit_getArgs_declRange__7___closed__1_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1050) << 1) | 1)),((lean_object*)(((size_t)(18) << 1) | 1))}};
static const lean_object* l_Lean_Doc_lit___regBuiltin_Lean_Doc_lit_getArgs_declRange__7___closed__1 = (const lean_object*)&l_Lean_Doc_lit___regBuiltin_Lean_Doc_lit_getArgs_declRange__7___closed__1_value;
static const lean_ctor_object l_Lean_Doc_lit___regBuiltin_Lean_Doc_lit_getArgs_declRange__7___closed__2_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*4 + 0, .m_other = 4, .m_tag = 0}, .m_objs = {((lean_object*)&l_Lean_Doc_lit___regBuiltin_Lean_Doc_lit_getArgs_declRange__7___closed__0_value),((lean_object*)(((size_t)(2) << 1) | 1)),((lean_object*)&l_Lean_Doc_lit___regBuiltin_Lean_Doc_lit_getArgs_declRange__7___closed__1_value),((lean_object*)(((size_t)(18) << 1) | 1))}};
static const lean_object* l_Lean_Doc_lit___regBuiltin_Lean_Doc_lit_getArgs_declRange__7___closed__2 = (const lean_object*)&l_Lean_Doc_lit___regBuiltin_Lean_Doc_lit_getArgs_declRange__7___closed__2_value;
@ -2655,9 +2655,9 @@ static const lean_string_object l_Lean_Doc_leanRole___regBuiltin_Lean_Doc_leanRo
static const lean_object* l_Lean_Doc_leanRole___regBuiltin_Lean_Doc_leanRole_getArgs_docString__5___closed__0 = (const lean_object*)&l_Lean_Doc_leanRole___regBuiltin_Lean_Doc_leanRole_getArgs_docString__5___closed__0_value;
LEAN_EXPORT lean_object* l_Lean_Doc_leanRole___regBuiltin_Lean_Doc_leanRole_getArgs_docString__5();
LEAN_EXPORT lean_object* l_Lean_Doc_leanRole___regBuiltin_Lean_Doc_leanRole_getArgs_docString__5___boxed(lean_object*);
static const lean_ctor_object l_Lean_Doc_leanRole___regBuiltin_Lean_Doc_leanRole_getArgs_declRange__7___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1076) << 1) | 1)),((lean_object*)(((size_t)(2) << 1) | 1))}};
static const lean_ctor_object l_Lean_Doc_leanRole___regBuiltin_Lean_Doc_leanRole_getArgs_declRange__7___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1080) << 1) | 1)),((lean_object*)(((size_t)(2) << 1) | 1))}};
static const lean_object* l_Lean_Doc_leanRole___regBuiltin_Lean_Doc_leanRole_getArgs_declRange__7___closed__0 = (const lean_object*)&l_Lean_Doc_leanRole___regBuiltin_Lean_Doc_leanRole_getArgs_declRange__7___closed__0_value;
static const lean_ctor_object l_Lean_Doc_leanRole___regBuiltin_Lean_Doc_leanRole_getArgs_declRange__7___closed__1_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1076) << 1) | 1)),((lean_object*)(((size_t)(23) << 1) | 1))}};
static const lean_ctor_object l_Lean_Doc_leanRole___regBuiltin_Lean_Doc_leanRole_getArgs_declRange__7___closed__1_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1080) << 1) | 1)),((lean_object*)(((size_t)(23) << 1) | 1))}};
static const lean_object* l_Lean_Doc_leanRole___regBuiltin_Lean_Doc_leanRole_getArgs_declRange__7___closed__1 = (const lean_object*)&l_Lean_Doc_leanRole___regBuiltin_Lean_Doc_leanRole_getArgs_declRange__7___closed__1_value;
static const lean_ctor_object l_Lean_Doc_leanRole___regBuiltin_Lean_Doc_leanRole_getArgs_declRange__7___closed__2_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*4 + 0, .m_other = 4, .m_tag = 0}, .m_objs = {((lean_object*)&l_Lean_Doc_leanRole___regBuiltin_Lean_Doc_leanRole_getArgs_declRange__7___closed__0_value),((lean_object*)(((size_t)(2) << 1) | 1)),((lean_object*)&l_Lean_Doc_leanRole___regBuiltin_Lean_Doc_leanRole_getArgs_declRange__7___closed__1_value),((lean_object*)(((size_t)(23) << 1) | 1))}};
static const lean_object* l_Lean_Doc_leanRole___regBuiltin_Lean_Doc_leanRole_getArgs_declRange__7___closed__2 = (const lean_object*)&l_Lean_Doc_leanRole___regBuiltin_Lean_Doc_leanRole_getArgs_declRange__7___closed__2_value;
@ -2690,9 +2690,9 @@ LEAN_EXPORT lean_object* l_Lean_Doc_leanTerm___regBuiltin_Lean_Doc_leanTerm__3()
LEAN_EXPORT lean_object* l_Lean_Doc_leanTerm___regBuiltin_Lean_Doc_leanTerm__3___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Doc_leanTerm___regBuiltin_Lean_Doc_leanTerm_getArgs_docString__5();
LEAN_EXPORT lean_object* l_Lean_Doc_leanTerm___regBuiltin_Lean_Doc_leanTerm_getArgs_docString__5___boxed(lean_object*);
static const lean_ctor_object l_Lean_Doc_leanTerm___regBuiltin_Lean_Doc_leanTerm_getArgs_declRange__7___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1104) << 1) | 1)),((lean_object*)(((size_t)(2) << 1) | 1))}};
static const lean_ctor_object l_Lean_Doc_leanTerm___regBuiltin_Lean_Doc_leanTerm_getArgs_declRange__7___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1108) << 1) | 1)),((lean_object*)(((size_t)(2) << 1) | 1))}};
static const lean_object* l_Lean_Doc_leanTerm___regBuiltin_Lean_Doc_leanTerm_getArgs_declRange__7___closed__0 = (const lean_object*)&l_Lean_Doc_leanTerm___regBuiltin_Lean_Doc_leanTerm_getArgs_declRange__7___closed__0_value;
static const lean_ctor_object l_Lean_Doc_leanTerm___regBuiltin_Lean_Doc_leanTerm_getArgs_declRange__7___closed__1_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1104) << 1) | 1)),((lean_object*)(((size_t)(24) << 1) | 1))}};
static const lean_ctor_object l_Lean_Doc_leanTerm___regBuiltin_Lean_Doc_leanTerm_getArgs_declRange__7___closed__1_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1108) << 1) | 1)),((lean_object*)(((size_t)(24) << 1) | 1))}};
static const lean_object* l_Lean_Doc_leanTerm___regBuiltin_Lean_Doc_leanTerm_getArgs_declRange__7___closed__1 = (const lean_object*)&l_Lean_Doc_leanTerm___regBuiltin_Lean_Doc_leanTerm_getArgs_declRange__7___closed__1_value;
static const lean_ctor_object l_Lean_Doc_leanTerm___regBuiltin_Lean_Doc_leanTerm_getArgs_declRange__7___closed__2_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*4 + 0, .m_other = 4, .m_tag = 0}, .m_objs = {((lean_object*)&l_Lean_Doc_leanTerm___regBuiltin_Lean_Doc_leanTerm_getArgs_declRange__7___closed__0_value),((lean_object*)(((size_t)(2) << 1) | 1)),((lean_object*)&l_Lean_Doc_leanTerm___regBuiltin_Lean_Doc_leanTerm_getArgs_declRange__7___closed__1_value),((lean_object*)(((size_t)(24) << 1) | 1))}};
static const lean_object* l_Lean_Doc_leanTerm___regBuiltin_Lean_Doc_leanTerm_getArgs_declRange__7___closed__2 = (const lean_object*)&l_Lean_Doc_leanTerm___regBuiltin_Lean_Doc_leanTerm_getArgs_declRange__7___closed__2_value;
@ -2800,9 +2800,9 @@ static const lean_string_object l_Lean_Doc_option___regBuiltin_Lean_Doc_option_g
static const lean_object* l_Lean_Doc_option___regBuiltin_Lean_Doc_option_getArgs_docString__5___closed__0 = (const lean_object*)&l_Lean_Doc_option___regBuiltin_Lean_Doc_option_getArgs_docString__5___closed__0_value;
LEAN_EXPORT lean_object* l_Lean_Doc_option___regBuiltin_Lean_Doc_option_getArgs_docString__5();
LEAN_EXPORT lean_object* l_Lean_Doc_option___regBuiltin_Lean_Doc_option_getArgs_docString__5___boxed(lean_object*);
static const lean_ctor_object l_Lean_Doc_option___regBuiltin_Lean_Doc_option_getArgs_declRange__7___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1132) << 1) | 1)),((lean_object*)(((size_t)(2) << 1) | 1))}};
static const lean_ctor_object l_Lean_Doc_option___regBuiltin_Lean_Doc_option_getArgs_declRange__7___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1136) << 1) | 1)),((lean_object*)(((size_t)(2) << 1) | 1))}};
static const lean_object* l_Lean_Doc_option___regBuiltin_Lean_Doc_option_getArgs_declRange__7___closed__0 = (const lean_object*)&l_Lean_Doc_option___regBuiltin_Lean_Doc_option_getArgs_declRange__7___closed__0_value;
static const lean_ctor_object l_Lean_Doc_option___regBuiltin_Lean_Doc_option_getArgs_declRange__7___closed__1_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1132) << 1) | 1)),((lean_object*)(((size_t)(18) << 1) | 1))}};
static const lean_ctor_object l_Lean_Doc_option___regBuiltin_Lean_Doc_option_getArgs_declRange__7___closed__1_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1136) << 1) | 1)),((lean_object*)(((size_t)(18) << 1) | 1))}};
static const lean_object* l_Lean_Doc_option___regBuiltin_Lean_Doc_option_getArgs_declRange__7___closed__1 = (const lean_object*)&l_Lean_Doc_option___regBuiltin_Lean_Doc_option_getArgs_declRange__7___closed__1_value;
static const lean_ctor_object l_Lean_Doc_option___regBuiltin_Lean_Doc_option_getArgs_declRange__7___closed__2_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*4 + 0, .m_other = 4, .m_tag = 0}, .m_objs = {((lean_object*)&l_Lean_Doc_option___regBuiltin_Lean_Doc_option_getArgs_declRange__7___closed__0_value),((lean_object*)(((size_t)(2) << 1) | 1)),((lean_object*)&l_Lean_Doc_option___regBuiltin_Lean_Doc_option_getArgs_declRange__7___closed__1_value),((lean_object*)(((size_t)(18) << 1) | 1))}};
static const lean_object* l_Lean_Doc_option___regBuiltin_Lean_Doc_option_getArgs_declRange__7___closed__2 = (const lean_object*)&l_Lean_Doc_option___regBuiltin_Lean_Doc_option_getArgs_declRange__7___closed__2_value;
@ -2880,9 +2880,9 @@ static const lean_string_object l_Lean_Doc_assert_x27___regBuiltin_Lean_Doc_asse
static const lean_object* l_Lean_Doc_assert_x27___regBuiltin_Lean_Doc_assert_x27_getArgs_docString__5___closed__0 = (const lean_object*)&l_Lean_Doc_assert_x27___regBuiltin_Lean_Doc_assert_x27_getArgs_docString__5___closed__0_value;
LEAN_EXPORT lean_object* l_Lean_Doc_assert_x27___regBuiltin_Lean_Doc_assert_x27_getArgs_docString__5();
LEAN_EXPORT lean_object* l_Lean_Doc_assert_x27___regBuiltin_Lean_Doc_assert_x27_getArgs_docString__5___boxed(lean_object*);
static const lean_ctor_object l_Lean_Doc_assert_x27___regBuiltin_Lean_Doc_assert_x27_getArgs_declRange__7___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1210) << 1) | 1)),((lean_object*)(((size_t)(2) << 1) | 1))}};
static const lean_ctor_object l_Lean_Doc_assert_x27___regBuiltin_Lean_Doc_assert_x27_getArgs_declRange__7___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1214) << 1) | 1)),((lean_object*)(((size_t)(2) << 1) | 1))}};
static const lean_object* l_Lean_Doc_assert_x27___regBuiltin_Lean_Doc_assert_x27_getArgs_declRange__7___closed__0 = (const lean_object*)&l_Lean_Doc_assert_x27___regBuiltin_Lean_Doc_assert_x27_getArgs_declRange__7___closed__0_value;
static const lean_ctor_object l_Lean_Doc_assert_x27___regBuiltin_Lean_Doc_assert_x27_getArgs_declRange__7___closed__1_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1210) << 1) | 1)),((lean_object*)(((size_t)(18) << 1) | 1))}};
static const lean_ctor_object l_Lean_Doc_assert_x27___regBuiltin_Lean_Doc_assert_x27_getArgs_declRange__7___closed__1_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1214) << 1) | 1)),((lean_object*)(((size_t)(18) << 1) | 1))}};
static const lean_object* l_Lean_Doc_assert_x27___regBuiltin_Lean_Doc_assert_x27_getArgs_declRange__7___closed__1 = (const lean_object*)&l_Lean_Doc_assert_x27___regBuiltin_Lean_Doc_assert_x27_getArgs_declRange__7___closed__1_value;
static const lean_ctor_object l_Lean_Doc_assert_x27___regBuiltin_Lean_Doc_assert_x27_getArgs_declRange__7___closed__2_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*4 + 0, .m_other = 4, .m_tag = 0}, .m_objs = {((lean_object*)&l_Lean_Doc_assert_x27___regBuiltin_Lean_Doc_assert_x27_getArgs_declRange__7___closed__0_value),((lean_object*)(((size_t)(2) << 1) | 1)),((lean_object*)&l_Lean_Doc_assert_x27___regBuiltin_Lean_Doc_assert_x27_getArgs_declRange__7___closed__1_value),((lean_object*)(((size_t)(18) << 1) | 1))}};
static const lean_object* l_Lean_Doc_assert_x27___regBuiltin_Lean_Doc_assert_x27_getArgs_declRange__7___closed__2 = (const lean_object*)&l_Lean_Doc_assert_x27___regBuiltin_Lean_Doc_assert_x27_getArgs_declRange__7___closed__2_value;
@ -2936,9 +2936,9 @@ static const lean_string_object l_Lean_Doc_assert___regBuiltin_Lean_Doc_assert_g
static const lean_object* l_Lean_Doc_assert___regBuiltin_Lean_Doc_assert_getArgs_docString__5___closed__0 = (const lean_object*)&l_Lean_Doc_assert___regBuiltin_Lean_Doc_assert_getArgs_docString__5___closed__0_value;
LEAN_EXPORT lean_object* l_Lean_Doc_assert___regBuiltin_Lean_Doc_assert_getArgs_docString__5();
LEAN_EXPORT lean_object* l_Lean_Doc_assert___regBuiltin_Lean_Doc_assert_getArgs_docString__5___boxed(lean_object*);
static const lean_ctor_object l_Lean_Doc_assert___regBuiltin_Lean_Doc_assert_getArgs_declRange__7___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1229) << 1) | 1)),((lean_object*)(((size_t)(2) << 1) | 1))}};
static const lean_ctor_object l_Lean_Doc_assert___regBuiltin_Lean_Doc_assert_getArgs_declRange__7___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1233) << 1) | 1)),((lean_object*)(((size_t)(2) << 1) | 1))}};
static const lean_object* l_Lean_Doc_assert___regBuiltin_Lean_Doc_assert_getArgs_declRange__7___closed__0 = (const lean_object*)&l_Lean_Doc_assert___regBuiltin_Lean_Doc_assert_getArgs_declRange__7___closed__0_value;
static const lean_ctor_object l_Lean_Doc_assert___regBuiltin_Lean_Doc_assert_getArgs_declRange__7___closed__1_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1229) << 1) | 1)),((lean_object*)(((size_t)(18) << 1) | 1))}};
static const lean_ctor_object l_Lean_Doc_assert___regBuiltin_Lean_Doc_assert_getArgs_declRange__7___closed__1_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1233) << 1) | 1)),((lean_object*)(((size_t)(18) << 1) | 1))}};
static const lean_object* l_Lean_Doc_assert___regBuiltin_Lean_Doc_assert_getArgs_declRange__7___closed__1 = (const lean_object*)&l_Lean_Doc_assert___regBuiltin_Lean_Doc_assert_getArgs_declRange__7___closed__1_value;
static const lean_ctor_object l_Lean_Doc_assert___regBuiltin_Lean_Doc_assert_getArgs_declRange__7___closed__2_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*4 + 0, .m_other = 4, .m_tag = 0}, .m_objs = {((lean_object*)&l_Lean_Doc_assert___regBuiltin_Lean_Doc_assert_getArgs_declRange__7___closed__0_value),((lean_object*)(((size_t)(2) << 1) | 1)),((lean_object*)&l_Lean_Doc_assert___regBuiltin_Lean_Doc_assert_getArgs_declRange__7___closed__1_value),((lean_object*)(((size_t)(18) << 1) | 1))}};
static const lean_object* l_Lean_Doc_assert___regBuiltin_Lean_Doc_assert_getArgs_declRange__7___closed__2 = (const lean_object*)&l_Lean_Doc_assert___regBuiltin_Lean_Doc_assert_getArgs_declRange__7___closed__2_value;
@ -3115,9 +3115,9 @@ static const lean_string_object l_Lean_Doc_open___regBuiltin_Lean_Doc_open_getAr
static const lean_object* l_Lean_Doc_open___regBuiltin_Lean_Doc_open_getArgs_docString__5___closed__0 = (const lean_object*)&l_Lean_Doc_open___regBuiltin_Lean_Doc_open_getArgs_docString__5___closed__0_value;
LEAN_EXPORT lean_object* l_Lean_Doc_open___regBuiltin_Lean_Doc_open_getArgs_docString__5();
LEAN_EXPORT lean_object* l_Lean_Doc_open___regBuiltin_Lean_Doc_open_getArgs_docString__5___boxed(lean_object*);
static const lean_ctor_object l_Lean_Doc_open___regBuiltin_Lean_Doc_open_getArgs_declRange__7___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1249) << 1) | 1)),((lean_object*)(((size_t)(2) << 1) | 1))}};
static const lean_ctor_object l_Lean_Doc_open___regBuiltin_Lean_Doc_open_getArgs_declRange__7___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1253) << 1) | 1)),((lean_object*)(((size_t)(2) << 1) | 1))}};
static const lean_object* l_Lean_Doc_open___regBuiltin_Lean_Doc_open_getArgs_declRange__7___closed__0 = (const lean_object*)&l_Lean_Doc_open___regBuiltin_Lean_Doc_open_getArgs_declRange__7___closed__0_value;
static const lean_ctor_object l_Lean_Doc_open___regBuiltin_Lean_Doc_open_getArgs_declRange__7___closed__1_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1249) << 1) | 1)),((lean_object*)(((size_t)(21) << 1) | 1))}};
static const lean_ctor_object l_Lean_Doc_open___regBuiltin_Lean_Doc_open_getArgs_declRange__7___closed__1_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1253) << 1) | 1)),((lean_object*)(((size_t)(21) << 1) | 1))}};
static const lean_object* l_Lean_Doc_open___regBuiltin_Lean_Doc_open_getArgs_declRange__7___closed__1 = (const lean_object*)&l_Lean_Doc_open___regBuiltin_Lean_Doc_open_getArgs_declRange__7___closed__1_value;
static const lean_ctor_object l_Lean_Doc_open___regBuiltin_Lean_Doc_open_getArgs_declRange__7___closed__2_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*4 + 0, .m_other = 4, .m_tag = 0}, .m_objs = {((lean_object*)&l_Lean_Doc_open___regBuiltin_Lean_Doc_open_getArgs_declRange__7___closed__0_value),((lean_object*)(((size_t)(2) << 1) | 1)),((lean_object*)&l_Lean_Doc_open___regBuiltin_Lean_Doc_open_getArgs_declRange__7___closed__1_value),((lean_object*)(((size_t)(21) << 1) | 1))}};
static const lean_object* l_Lean_Doc_open___regBuiltin_Lean_Doc_open_getArgs_declRange__7___closed__2 = (const lean_object*)&l_Lean_Doc_open___regBuiltin_Lean_Doc_open_getArgs_declRange__7___closed__2_value;
@ -3162,9 +3162,9 @@ static const lean_string_object l_Lean_Doc_set__option___regBuiltin_Lean_Doc_set
static const lean_object* l_Lean_Doc_set__option___regBuiltin_Lean_Doc_set__option_getArgs_docString__5___closed__0 = (const lean_object*)&l_Lean_Doc_set__option___regBuiltin_Lean_Doc_set__option_getArgs_docString__5___closed__0_value;
LEAN_EXPORT lean_object* l_Lean_Doc_set__option___regBuiltin_Lean_Doc_set__option_getArgs_docString__5();
LEAN_EXPORT lean_object* l_Lean_Doc_set__option___regBuiltin_Lean_Doc_set__option_getArgs_docString__5___boxed(lean_object*);
static const lean_ctor_object l_Lean_Doc_set__option___regBuiltin_Lean_Doc_set__option_getArgs_declRange__7___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1272) << 1) | 1)),((lean_object*)(((size_t)(2) << 1) | 1))}};
static const lean_ctor_object l_Lean_Doc_set__option___regBuiltin_Lean_Doc_set__option_getArgs_declRange__7___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1276) << 1) | 1)),((lean_object*)(((size_t)(2) << 1) | 1))}};
static const lean_object* l_Lean_Doc_set__option___regBuiltin_Lean_Doc_set__option_getArgs_declRange__7___closed__0 = (const lean_object*)&l_Lean_Doc_set__option___regBuiltin_Lean_Doc_set__option_getArgs_declRange__7___closed__0_value;
static const lean_ctor_object l_Lean_Doc_set__option___regBuiltin_Lean_Doc_set__option_getArgs_declRange__7___closed__1_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1272) << 1) | 1)),((lean_object*)(((size_t)(21) << 1) | 1))}};
static const lean_ctor_object l_Lean_Doc_set__option___regBuiltin_Lean_Doc_set__option_getArgs_declRange__7___closed__1_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1276) << 1) | 1)),((lean_object*)(((size_t)(21) << 1) | 1))}};
static const lean_object* l_Lean_Doc_set__option___regBuiltin_Lean_Doc_set__option_getArgs_declRange__7___closed__1 = (const lean_object*)&l_Lean_Doc_set__option___regBuiltin_Lean_Doc_set__option_getArgs_declRange__7___closed__1_value;
static const lean_ctor_object l_Lean_Doc_set__option___regBuiltin_Lean_Doc_set__option_getArgs_declRange__7___closed__2_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*4 + 0, .m_other = 4, .m_tag = 0}, .m_objs = {((lean_object*)&l_Lean_Doc_set__option___regBuiltin_Lean_Doc_set__option_getArgs_declRange__7___closed__0_value),((lean_object*)(((size_t)(2) << 1) | 1)),((lean_object*)&l_Lean_Doc_set__option___regBuiltin_Lean_Doc_set__option_getArgs_declRange__7___closed__1_value),((lean_object*)(((size_t)(21) << 1) | 1))}};
static const lean_object* l_Lean_Doc_set__option___regBuiltin_Lean_Doc_set__option_getArgs_declRange__7___closed__2 = (const lean_object*)&l_Lean_Doc_set__option___regBuiltin_Lean_Doc_set__option_getArgs_declRange__7___closed__2_value;
@ -3235,9 +3235,9 @@ static const lean_string_object l_Lean_Doc_manual___regBuiltin_Lean_Doc_manual_g
static const lean_object* l_Lean_Doc_manual___regBuiltin_Lean_Doc_manual_getArgs_docString__5___closed__0 = (const lean_object*)&l_Lean_Doc_manual___regBuiltin_Lean_Doc_manual_getArgs_docString__5___closed__0_value;
LEAN_EXPORT lean_object* l_Lean_Doc_manual___regBuiltin_Lean_Doc_manual_getArgs_docString__5();
LEAN_EXPORT lean_object* l_Lean_Doc_manual___regBuiltin_Lean_Doc_manual_getArgs_docString__5___boxed(lean_object*);
static const lean_ctor_object l_Lean_Doc_manual___regBuiltin_Lean_Doc_manual_getArgs_declRange__7___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1288) << 1) | 1)),((lean_object*)(((size_t)(2) << 1) | 1))}};
static const lean_ctor_object l_Lean_Doc_manual___regBuiltin_Lean_Doc_manual_getArgs_declRange__7___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1292) << 1) | 1)),((lean_object*)(((size_t)(2) << 1) | 1))}};
static const lean_object* l_Lean_Doc_manual___regBuiltin_Lean_Doc_manual_getArgs_declRange__7___closed__0 = (const lean_object*)&l_Lean_Doc_manual___regBuiltin_Lean_Doc_manual_getArgs_declRange__7___closed__0_value;
static const lean_ctor_object l_Lean_Doc_manual___regBuiltin_Lean_Doc_manual_getArgs_declRange__7___closed__1_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1288) << 1) | 1)),((lean_object*)(((size_t)(18) << 1) | 1))}};
static const lean_ctor_object l_Lean_Doc_manual___regBuiltin_Lean_Doc_manual_getArgs_declRange__7___closed__1_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 0, .m_other = 2, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(1292) << 1) | 1)),((lean_object*)(((size_t)(18) << 1) | 1))}};
static const lean_object* l_Lean_Doc_manual___regBuiltin_Lean_Doc_manual_getArgs_declRange__7___closed__1 = (const lean_object*)&l_Lean_Doc_manual___regBuiltin_Lean_Doc_manual_getArgs_declRange__7___closed__1_value;
static const lean_ctor_object l_Lean_Doc_manual___regBuiltin_Lean_Doc_manual_getArgs_declRange__7___closed__2_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*4 + 0, .m_other = 4, .m_tag = 0}, .m_objs = {((lean_object*)&l_Lean_Doc_manual___regBuiltin_Lean_Doc_manual_getArgs_declRange__7___closed__0_value),((lean_object*)(((size_t)(2) << 1) | 1)),((lean_object*)&l_Lean_Doc_manual___regBuiltin_Lean_Doc_manual_getArgs_declRange__7___closed__1_value),((lean_object*)(((size_t)(18) << 1) | 1))}};
static const lean_object* l_Lean_Doc_manual___regBuiltin_Lean_Doc_manual_getArgs_declRange__7___closed__2 = (const lean_object*)&l_Lean_Doc_manual___regBuiltin_Lean_Doc_manual_getArgs_declRange__7___closed__2_value;
@ -48466,9 +48466,10 @@ lean_ctor_set(x_37, 7, x_31);
lean_ctor_set(x_37, 8, x_33);
lean_ctor_set(x_37, 9, x_35);
lean_ctor_set(x_37, 10, x_36);
x_38 = lean_alloc_ctor(0, 1, 1);
x_38 = lean_alloc_ctor(0, 1, 2);
lean_ctor_set(x_38, 0, x_6);
lean_ctor_set_uint8(x_38, sizeof(void*)*1, x_7);
lean_ctor_set_uint8(x_38, sizeof(void*)*1 + 1, x_7);
x_39 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_39, 0, x_36);
lean_ctor_set(x_39, 1, x_38);
@ -49348,7 +49349,7 @@ return x_44;
}
else
{
lean_object* x_45; lean_object* x_46; lean_object* x_47; uint8_t x_48; uint8_t x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; uint8_t x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; uint8_t x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_119; lean_object* x_120; uint8_t x_121; lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125; lean_object* x_126; lean_object* x_127; lean_object* x_128; lean_object* x_129; lean_object* x_150; lean_object* x_151; lean_object* x_152; uint8_t x_153; lean_object* x_154; lean_object* x_155; lean_object* x_156; lean_object* x_157; lean_object* x_158; lean_object* x_159; lean_object* x_160; lean_object* x_161; lean_object* x_162; lean_object* x_174; lean_object* x_175; uint8_t x_176; lean_object* x_177; lean_object* x_178; lean_object* x_179; lean_object* x_180; lean_object* x_181; lean_object* x_182; lean_object* x_183; lean_object* x_184; lean_object* x_205; lean_object* x_206; lean_object* x_207;
lean_object* x_45; lean_object* x_46; lean_object* x_47; uint8_t x_48; uint8_t x_49; lean_object* x_50; uint8_t x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_77; uint8_t x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_119; lean_object* x_120; uint8_t x_121; lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125; lean_object* x_126; lean_object* x_127; lean_object* x_128; lean_object* x_129; lean_object* x_150; lean_object* x_151; lean_object* x_152; lean_object* x_153; uint8_t x_154; lean_object* x_155; lean_object* x_156; lean_object* x_157; lean_object* x_158; lean_object* x_159; lean_object* x_160; lean_object* x_161; lean_object* x_162; lean_object* x_174; lean_object* x_175; uint8_t x_176; lean_object* x_177; lean_object* x_178; lean_object* x_179; lean_object* x_180; lean_object* x_181; lean_object* x_182; lean_object* x_183; lean_object* x_184; lean_object* x_205; lean_object* x_206; lean_object* x_207;
x_45 = lean_array_uget_borrowed(x_6, x_8);
x_46 = lean_ctor_get(x_45, 1);
x_47 = lean_ctor_get(x_45, 2);
@ -49380,16 +49381,16 @@ block_76:
{
lean_object* x_64; lean_object* x_65;
x_64 = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(x_64, 0, x_62);
lean_ctor_set(x_64, 0, x_52);
lean_ctor_set(x_64, 1, x_63);
lean_inc(x_54);
lean_inc_ref(x_53);
lean_inc(x_55);
lean_inc_ref(x_59);
lean_inc(x_58);
lean_inc_ref(x_55);
lean_inc(x_56);
lean_inc_ref(x_58);
x_65 = l_Lean_logErrorAt___at___00Lean_Doc_name_spec__2___redArg(x_57, x_64, x_52, x_58, x_56, x_59, x_55, x_53, x_54);
lean_dec(x_57);
lean_inc_ref(x_53);
lean_inc(x_57);
lean_inc_ref(x_60);
x_65 = l_Lean_logErrorAt___at___00Lean_Doc_name_spec__2___redArg(x_54, x_64, x_59, x_60, x_57, x_53, x_56, x_55, x_58);
lean_dec(x_54);
if (lean_obj_tag(x_65) == 0)
{
lean_object* x_66; lean_object* x_67;
@ -49397,20 +49398,20 @@ x_66 = lean_ctor_get(x_65, 0);
lean_inc(x_66);
lean_dec_ref(x_65);
lean_inc(x_3);
x_67 = l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Doc_lean_spec__5___lam__2(x_3, x_51, x_66, x_60, x_61, x_52, x_58, x_56, x_59, x_55, x_53, x_54);
x_67 = l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Doc_lean_spec__5___lam__2(x_3, x_62, x_66, x_51, x_61, x_59, x_60, x_57, x_53, x_56, x_55, x_58);
x_20 = x_67;
goto block_42;
}
else
{
lean_object* x_68; lean_object* x_69; uint8_t x_70; uint8_t x_75;
lean_dec_ref(x_59);
lean_dec_ref(x_58);
lean_dec_ref(x_62);
lean_dec_ref(x_60);
lean_dec(x_58);
lean_dec(x_57);
lean_dec(x_56);
lean_dec(x_55);
lean_dec(x_54);
lean_dec_ref(x_55);
lean_dec_ref(x_53);
lean_dec_ref(x_51);
lean_dec(x_18);
lean_dec_ref(x_17);
lean_dec(x_16);
@ -49460,25 +49461,25 @@ return x_71;
block_118:
{
lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; uint8_t x_100; lean_object* x_101; uint8_t x_102; lean_object* x_103; uint8_t x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107;
x_88 = lean_ctor_get(x_79, 0);
x_89 = lean_ctor_get(x_79, 1);
x_90 = lean_ctor_get(x_79, 2);
x_91 = lean_ctor_get(x_79, 3);
x_92 = lean_ctor_get(x_79, 4);
x_93 = lean_ctor_get(x_79, 5);
x_94 = lean_ctor_get(x_79, 6);
x_95 = lean_ctor_get(x_79, 7);
x_96 = lean_ctor_get(x_79, 8);
x_97 = lean_ctor_get(x_79, 9);
x_98 = lean_ctor_get(x_79, 10);
x_99 = lean_ctor_get(x_79, 11);
x_100 = lean_ctor_get_uint8(x_79, sizeof(void*)*14);
x_101 = lean_ctor_get(x_79, 12);
x_102 = lean_ctor_get_uint8(x_79, sizeof(void*)*14 + 1);
x_103 = lean_ctor_get(x_79, 13);
x_88 = lean_ctor_get(x_81, 0);
x_89 = lean_ctor_get(x_81, 1);
x_90 = lean_ctor_get(x_81, 2);
x_91 = lean_ctor_get(x_81, 3);
x_92 = lean_ctor_get(x_81, 4);
x_93 = lean_ctor_get(x_81, 5);
x_94 = lean_ctor_get(x_81, 6);
x_95 = lean_ctor_get(x_81, 7);
x_96 = lean_ctor_get(x_81, 8);
x_97 = lean_ctor_get(x_81, 9);
x_98 = lean_ctor_get(x_81, 10);
x_99 = lean_ctor_get(x_81, 11);
x_100 = lean_ctor_get_uint8(x_81, sizeof(void*)*14);
x_101 = lean_ctor_get(x_81, 12);
x_102 = lean_ctor_get_uint8(x_81, sizeof(void*)*14 + 1);
x_103 = lean_ctor_get(x_81, 13);
x_104 = 0;
x_105 = l_Lean_replaceRef(x_87, x_93);
lean_dec(x_87);
x_105 = l_Lean_replaceRef(x_80, x_93);
lean_dec(x_80);
lean_inc_ref(x_103);
lean_inc(x_101);
lean_inc(x_99);
@ -49509,13 +49510,13 @@ lean_ctor_set(x_106, 12, x_101);
lean_ctor_set(x_106, 13, x_103);
lean_ctor_set_uint8(x_106, sizeof(void*)*14, x_100);
lean_ctor_set_uint8(x_106, sizeof(void*)*14 + 1, x_102);
lean_inc(x_82);
lean_inc(x_83);
lean_inc_ref(x_85);
lean_inc(x_82);
lean_inc_ref(x_79);
lean_inc(x_84);
lean_inc_ref(x_86);
lean_inc(x_50);
x_107 = l_Lean_log___at___00Lean_logWarning___at___00Lean_checkPrivateInPublic___at___00Lean_resolveGlobalName___at___00__private_Lean_ResolveName_0__Lean_resolveLocalName_loop___at___00Lean_resolveLocalName___at___00Lean_unresolveNameGlobalAvoidingLocals_x3f___at___00Lean_unresolveNameGlobalAvoidingLocals___at___00__private_Lean_Elab_DocString_Builtin_0__Lean_Doc_getQualified_spec__0_spec__0_spec__1_spec__8_spec__14_spec__21_spec__28_spec__33(x_50, x_104, x_43, x_81, x_80, x_78, x_86, x_84, x_85, x_83, x_106, x_82);
x_107 = l_Lean_log___at___00Lean_logWarning___at___00Lean_checkPrivateInPublic___at___00Lean_resolveGlobalName___at___00__private_Lean_ResolveName_0__Lean_resolveLocalName_loop___at___00Lean_resolveLocalName___at___00Lean_unresolveNameGlobalAvoidingLocals_x3f___at___00Lean_unresolveNameGlobalAvoidingLocals___at___00__private_Lean_Elab_DocString_Builtin_0__Lean_Doc_getQualified_spec__0_spec__0_spec__1_spec__8_spec__14_spec__21_spec__28_spec__33(x_50, x_104, x_43, x_78, x_87, x_85, x_86, x_84, x_79, x_82, x_106, x_83);
if (lean_obj_tag(x_107) == 0)
{
lean_object* x_108; lean_object* x_109;
@ -49523,7 +49524,7 @@ x_108 = lean_ctor_get(x_107, 0);
lean_inc(x_108);
lean_dec_ref(x_107);
lean_inc(x_3);
x_109 = l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Doc_lean_spec__5___lam__2(x_3, x_77, x_108, x_81, x_80, x_78, x_86, x_84, x_85, x_83, x_79, x_82);
x_109 = l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___00Lean_Doc_lean_spec__5___lam__2(x_3, x_77, x_108, x_78, x_87, x_85, x_86, x_84, x_79, x_82, x_81, x_83);
x_20 = x_109;
goto block_42;
}
@ -49531,10 +49532,10 @@ else
{
lean_object* x_110; lean_object* x_111; uint8_t x_112; uint8_t x_117;
lean_dec_ref(x_86);
lean_dec_ref(x_85);
lean_dec(x_84);
lean_dec(x_83);
lean_dec(x_82);
lean_dec_ref(x_81);
lean_dec_ref(x_79);
lean_dec_ref(x_77);
lean_dec(x_18);
@ -49591,16 +49592,16 @@ x_131 = l_Lean_instBEqMessageSeverity_beq(x_48, x_130);
if (x_131 == 0)
{
x_77 = x_119;
x_78 = x_123;
x_79 = x_128;
x_80 = x_122;
x_81 = x_121;
x_82 = x_129;
x_83 = x_127;
x_78 = x_121;
x_79 = x_126;
x_80 = x_120;
x_81 = x_128;
x_82 = x_127;
x_83 = x_129;
x_84 = x_125;
x_85 = x_126;
x_85 = x_123;
x_86 = x_124;
x_87 = x_120;
x_87 = x_122;
goto block_118;
}
else
@ -49610,16 +49611,16 @@ if (x_4 == 0)
if (x_131 == 0)
{
x_77 = x_119;
x_78 = x_123;
x_79 = x_128;
x_80 = x_122;
x_81 = x_121;
x_82 = x_129;
x_83 = x_127;
x_78 = x_121;
x_79 = x_126;
x_80 = x_120;
x_81 = x_128;
x_82 = x_127;
x_83 = x_129;
x_84 = x_125;
x_85 = x_126;
x_85 = x_123;
x_86 = x_124;
x_87 = x_120;
x_87 = x_122;
goto block_118;
}
else
@ -49650,18 +49651,18 @@ if (lean_obj_tag(x_135) == 0)
{
lean_object* x_139;
x_139 = lean_obj_once(&l___private_Lean_ExtraModUses_0__Lean_recordExtraModUseCore___at___00Lean_recordExtraModUseFromDecl___at___00__private_Lean_Elab_DocString_Builtin_0__Lean_Doc_elabExtraTerm_spec__0_spec__0___closed__13, &l___private_Lean_ExtraModUses_0__Lean_recordExtraModUseCore___at___00Lean_recordExtraModUseFromDecl___at___00__private_Lean_Elab_DocString_Builtin_0__Lean_Doc_elabExtraTerm_spec__0_spec__0___closed__13_once, _init_l___private_Lean_ExtraModUses_0__Lean_recordExtraModUseCore___at___00Lean_recordExtraModUseFromDecl___at___00__private_Lean_Elab_DocString_Builtin_0__Lean_Doc_elabExtraTerm_spec__0_spec__0___closed__13);
x_51 = x_119;
x_52 = x_123;
x_53 = x_128;
x_54 = x_129;
x_55 = x_127;
x_56 = x_125;
x_57 = x_120;
x_58 = x_124;
x_59 = x_126;
x_60 = x_121;
x_51 = x_121;
x_52 = x_138;
x_53 = x_126;
x_54 = x_120;
x_55 = x_128;
x_56 = x_127;
x_57 = x_125;
x_58 = x_129;
x_59 = x_123;
x_60 = x_124;
x_61 = x_122;
x_62 = x_138;
x_62 = x_119;
x_63 = x_139;
goto block_76;
}
@ -49671,18 +49672,18 @@ lean_object* x_140;
x_140 = lean_ctor_get(x_135, 0);
lean_inc(x_140);
lean_dec_ref(x_135);
x_51 = x_119;
x_52 = x_123;
x_53 = x_128;
x_54 = x_129;
x_55 = x_127;
x_56 = x_125;
x_57 = x_120;
x_58 = x_124;
x_59 = x_126;
x_60 = x_121;
x_51 = x_121;
x_52 = x_138;
x_53 = x_126;
x_54 = x_120;
x_55 = x_128;
x_56 = x_127;
x_57 = x_125;
x_58 = x_129;
x_59 = x_123;
x_60 = x_124;
x_61 = x_122;
x_62 = x_138;
x_62 = x_119;
x_63 = x_140;
goto block_76;
}
@ -49748,16 +49749,16 @@ return x_144;
else
{
x_77 = x_119;
x_78 = x_123;
x_79 = x_128;
x_80 = x_122;
x_81 = x_121;
x_82 = x_129;
x_83 = x_127;
x_78 = x_121;
x_79 = x_126;
x_80 = x_120;
x_81 = x_128;
x_82 = x_127;
x_83 = x_129;
x_84 = x_125;
x_85 = x_126;
x_85 = x_123;
x_86 = x_124;
x_87 = x_120;
x_87 = x_122;
goto block_118;
}
}
@ -49766,42 +49767,42 @@ block_173:
{
lean_object* x_163; lean_object* x_164;
x_163 = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(x_163, 0, x_161);
lean_ctor_set(x_163, 0, x_157);
lean_ctor_set(x_163, 1, x_162);
lean_inc(x_161);
lean_inc_ref(x_150);
lean_inc(x_155);
lean_inc_ref(x_159);
lean_inc(x_150);
lean_inc_ref(x_157);
lean_inc(x_152);
lean_inc_ref(x_160);
x_164 = l_Lean_logErrorAt___at___00Lean_Doc_name_spec__2___redArg(x_156, x_163, x_154, x_160, x_152, x_157, x_150, x_159, x_155);
lean_inc(x_151);
lean_inc_ref(x_156);
x_164 = l_Lean_logErrorAt___at___00Lean_Doc_name_spec__2___redArg(x_153, x_163, x_152, x_156, x_151, x_159, x_155, x_150, x_161);
if (lean_obj_tag(x_164) == 0)
{
lean_dec_ref(x_164);
x_119 = x_151;
x_120 = x_156;
x_121 = x_153;
x_122 = x_158;
x_123 = x_154;
x_124 = x_160;
x_125 = x_152;
x_126 = x_157;
x_127 = x_150;
x_128 = x_159;
x_129 = x_155;
x_119 = x_158;
x_120 = x_153;
x_121 = x_154;
x_122 = x_160;
x_123 = x_152;
x_124 = x_156;
x_125 = x_151;
x_126 = x_159;
x_127 = x_155;
x_128 = x_150;
x_129 = x_161;
goto block_149;
}
else
{
lean_object* x_165; lean_object* x_166; uint8_t x_167; uint8_t x_172;
lean_dec_ref(x_160);
lean_dec(x_161);
lean_dec_ref(x_159);
lean_dec_ref(x_157);
lean_dec(x_156);
lean_dec_ref(x_158);
lean_dec_ref(x_156);
lean_dec(x_155);
lean_dec(x_152);
lean_dec_ref(x_151);
lean_dec(x_150);
lean_dec(x_153);
lean_dec(x_151);
lean_dec_ref(x_150);
lean_dec(x_18);
lean_dec_ref(x_17);
lean_dec(x_16);
@ -49915,18 +49916,18 @@ if (lean_obj_tag(x_190) == 0)
{
lean_object* x_194;
x_194 = lean_obj_once(&l___private_Lean_ExtraModUses_0__Lean_recordExtraModUseCore___at___00Lean_recordExtraModUseFromDecl___at___00__private_Lean_Elab_DocString_Builtin_0__Lean_Doc_elabExtraTerm_spec__0_spec__0___closed__13, &l___private_Lean_ExtraModUses_0__Lean_recordExtraModUseCore___at___00Lean_recordExtraModUseFromDecl___at___00__private_Lean_Elab_DocString_Builtin_0__Lean_Doc_elabExtraTerm_spec__0_spec__0___closed__13_once, _init_l___private_Lean_ExtraModUses_0__Lean_recordExtraModUseCore___at___00Lean_recordExtraModUseFromDecl___at___00__private_Lean_Elab_DocString_Builtin_0__Lean_Doc_elabExtraTerm_spec__0_spec__0___closed__13);
x_150 = x_182;
x_151 = x_175;
x_152 = x_180;
x_153 = x_176;
x_154 = x_178;
x_155 = x_184;
x_156 = x_174;
x_157 = x_181;
x_158 = x_177;
x_159 = x_183;
x_160 = x_179;
x_161 = x_193;
x_150 = x_183;
x_151 = x_180;
x_152 = x_178;
x_153 = x_174;
x_154 = x_176;
x_155 = x_182;
x_156 = x_179;
x_157 = x_193;
x_158 = x_175;
x_159 = x_181;
x_160 = x_177;
x_161 = x_184;
x_162 = x_194;
goto block_173;
}
@ -49936,18 +49937,18 @@ lean_object* x_195;
x_195 = lean_ctor_get(x_190, 0);
lean_inc(x_195);
lean_dec_ref(x_190);
x_150 = x_182;
x_151 = x_175;
x_152 = x_180;
x_153 = x_176;
x_154 = x_178;
x_155 = x_184;
x_156 = x_174;
x_157 = x_181;
x_158 = x_177;
x_159 = x_183;
x_160 = x_179;
x_161 = x_193;
x_150 = x_183;
x_151 = x_180;
x_152 = x_178;
x_153 = x_174;
x_154 = x_176;
x_155 = x_182;
x_156 = x_179;
x_157 = x_193;
x_158 = x_175;
x_159 = x_181;
x_160 = x_177;
x_161 = x_184;
x_162 = x_195;
goto block_173;
}
@ -52639,8 +52640,8 @@ return x_130;
else
{
lean_dec(x_18);
lean_dec(x_17);
lean_dec_ref(x_2);
lean_dec(x_17);
lean_dec(x_12);
lean_dec_ref(x_11);
lean_dec(x_10);

62
stage0/stdlib/Lean/Elab/Frontend.c generated
View file

@ -118,7 +118,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_IO_processCommandsIncrementally(lean_object
LEAN_EXPORT lean_object* l_Lean_Elab_IO_processCommandsIncrementally___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_IO_processCommands(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_IO_processCommands___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static const lean_ctor_object l_Lean_Elab_process___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*1 + 8, .m_other = 1, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(0) << 1) | 1)),LEAN_SCALAR_PTR_LITERAL(0, 0, 0, 0, 0, 0, 0, 0)}};
static const lean_ctor_object l_Lean_Elab_process___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*1 + 8, .m_other = 1, .m_tag = 0}, .m_objs = {((lean_object*)(((size_t)(0) << 1) | 1)),LEAN_SCALAR_PTR_LITERAL(0, 1, 0, 0, 0, 0, 0, 0)}};
static const lean_object* l_Lean_Elab_process___closed__0 = (const lean_object*)&l_Lean_Elab_process___closed__0_value;
static const lean_string_object l_Lean_Elab_process___closed__1_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 8, .m_capacity = 8, .m_length = 7, .m_data = "<input>"};
static const lean_object* l_Lean_Elab_process___closed__1 = (const lean_object*)&l_Lean_Elab_process___closed__1_value;
@ -2404,7 +2404,7 @@ return x_8;
LEAN_EXPORT lean_object* l_Lean_Elab_runFrontend___lam__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, uint32_t x_5, uint8_t x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
_start:
{
lean_object* x_11; lean_object* x_12; uint8_t x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
lean_object* x_11; lean_object* x_12; lean_object* x_13; uint8_t x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
if (lean_obj_tag(x_1) == 1)
{
lean_object* x_25; lean_object* x_26; lean_object* x_27; uint8_t x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_39; lean_object* x_49; lean_object* x_50; uint8_t x_51;
@ -2479,12 +2479,12 @@ if (lean_obj_tag(x_29) == 0)
{
lean_object* x_36;
x_36 = l_Lean_Elab_HeaderSyntax_imports(x_8, x_6);
x_11 = x_27;
x_12 = x_26;
x_13 = x_35;
x_14 = x_32;
x_15 = x_33;
x_16 = x_30;
x_11 = x_33;
x_12 = x_30;
x_13 = x_32;
x_14 = x_35;
x_15 = x_27;
x_16 = x_26;
x_17 = x_36;
goto block_24;
}
@ -2495,12 +2495,12 @@ lean_dec(x_8);
x_37 = lean_ctor_get(x_29, 0);
lean_inc(x_37);
lean_dec_ref(x_29);
x_11 = x_27;
x_12 = x_26;
x_13 = x_35;
x_14 = x_32;
x_15 = x_33;
x_16 = x_30;
x_11 = x_33;
x_12 = x_30;
x_13 = x_32;
x_14 = x_35;
x_15 = x_27;
x_16 = x_26;
x_17 = x_37;
goto block_24;
}
@ -2592,18 +2592,18 @@ return x_66;
block_24:
{
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_18 = l_Lean_LeanOptions_toOptions(x_15);
x_18 = l_Lean_LeanOptions_toOptions(x_11);
x_19 = l_Lean_Options_mergeBy(x_2, x_3, x_18);
x_20 = l_Array_append___redArg(x_4, x_14);
lean_dec_ref(x_14);
x_20 = l_Array_append___redArg(x_4, x_13);
lean_dec_ref(x_13);
x_21 = lean_alloc_ctor(0, 6, 5);
lean_ctor_set(x_21, 0, x_12);
lean_ctor_set(x_21, 1, x_11);
lean_ctor_set(x_21, 0, x_16);
lean_ctor_set(x_21, 1, x_15);
lean_ctor_set(x_21, 2, x_17);
lean_ctor_set(x_21, 3, x_19);
lean_ctor_set(x_21, 4, x_16);
lean_ctor_set(x_21, 4, x_12);
lean_ctor_set(x_21, 5, x_20);
lean_ctor_set_uint8(x_21, sizeof(void*)*6 + 4, x_13);
lean_ctor_set_uint8(x_21, sizeof(void*)*6 + 4, x_14);
lean_ctor_set_uint32(x_21, sizeof(void*)*6, x_5);
x_22 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_22, 0, x_21);
@ -3014,7 +3014,7 @@ return x_2;
LEAN_EXPORT lean_object* l_Lean_Elab_runFrontend(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, uint32_t x_5, lean_object* x_6, lean_object* x_7, uint8_t x_8, lean_object* x_9, lean_object* x_10, uint8_t x_11, lean_object* x_12) {
_start:
{
lean_object* x_14; lean_object* x_15; lean_object* x_20; lean_object* x_21; uint8_t x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; double x_40; double x_41; double x_42; lean_object* x_43; lean_object* x_44; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_100; lean_object* x_101; lean_object* x_102; uint8_t x_116; lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* x_136; lean_object* x_137; lean_object* x_138; lean_object* x_175;
lean_object* x_14; lean_object* x_15; lean_object* x_20; lean_object* x_21; uint8_t x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; double x_40; double x_41; double x_42; lean_object* x_43; lean_object* x_44; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_116; lean_object* x_117; lean_object* x_118; uint8_t x_119; lean_object* x_120; lean_object* x_136; lean_object* x_137; lean_object* x_138; lean_object* x_175;
x_20 = lean_io_mono_nanos_now();
x_21 = ((lean_object*)(l_Lean_Elab_runFrontend___closed__0));
x_22 = 1;
@ -3414,7 +3414,7 @@ goto block_74;
}
block_135:
{
if (x_116 == 0)
if (x_119 == 0)
{
if (lean_obj_tag(x_6) == 1)
{
@ -3428,8 +3428,8 @@ x_123 = lean_alloc_closure((void*)(l_Lean_writeModule___boxed), 3, 2);
lean_closure_set(x_123, 0, x_118);
lean_closure_set(x_123, 1, x_121);
x_124 = lean_box(0);
x_125 = l_Lean_profileitIOUnsafe___redArg(x_122, x_119, x_123, x_124);
lean_dec_ref(x_119);
x_125 = l_Lean_profileitIOUnsafe___redArg(x_122, x_116, x_123, x_124);
lean_dec_ref(x_116);
if (lean_obj_tag(x_125) == 0)
{
lean_dec_ref(x_125);
@ -3489,7 +3489,7 @@ return x_129;
}
else
{
lean_dec_ref(x_119);
lean_dec_ref(x_116);
lean_dec(x_6);
x_100 = x_117;
x_101 = x_118;
@ -3501,9 +3501,9 @@ else
{
lean_object* x_134;
lean_dec_ref(x_120);
lean_dec_ref(x_119);
lean_dec_ref(x_118);
lean_dec(x_117);
lean_dec_ref(x_116);
lean_dec(x_36);
lean_dec_ref(x_28);
lean_dec_ref(x_24);
@ -3566,10 +3566,10 @@ lean_inc_ref(x_148);
lean_dec(x_147);
x_149 = lean_unbox(x_140);
lean_dec(x_140);
x_116 = x_149;
x_116 = x_148;
x_117 = x_136;
x_118 = x_145;
x_119 = x_148;
x_119 = x_149;
x_120 = x_137;
goto block_135;
}
@ -3587,10 +3587,10 @@ uint8_t x_152;
lean_dec_ref(x_151);
x_152 = lean_unbox(x_140);
lean_dec(x_140);
x_116 = x_152;
x_116 = x_150;
x_117 = x_136;
x_118 = x_145;
x_119 = x_150;
x_119 = x_152;
x_120 = x_137;
goto block_135;
}

2254
stage0/stdlib/Lean/Elab/MutualDef.c generated
View file

File diff suppressed because it is too large Load diff

334
stage0/stdlib/Lean/Elab/StructInstHint.c generated
View file

@ -1930,7 +1930,7 @@ goto block_224;
}
block_224:
{
uint8_t x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_92; lean_object* x_93; uint8_t x_94; lean_object* x_95; lean_object* x_96; uint8_t x_97; lean_object* x_98; lean_object* x_99; lean_object* x_100; lean_object* x_101; lean_object* x_108; lean_object* x_109; lean_object* x_110; uint8_t x_111; lean_object* x_112; uint8_t x_113; lean_object* x_114; lean_object* x_115; lean_object* x_116; lean_object* x_117; lean_object* x_120; lean_object* x_121; lean_object* x_122; lean_object* x_123; lean_object* x_124; uint8_t x_125; lean_object* x_126; uint8_t x_127; lean_object* x_128; lean_object* x_129; lean_object* x_130; lean_object* x_131; lean_object* x_141; lean_object* x_142; lean_object* x_143; lean_object* x_144; uint8_t x_145; lean_object* x_146; lean_object* x_147; uint8_t x_148; lean_object* x_149; lean_object* x_150; lean_object* x_151; lean_object* x_155; lean_object* x_156; lean_object* x_157; lean_object* x_158; lean_object* x_159; lean_object* x_186; lean_object* x_187; lean_object* x_188; lean_object* x_189; lean_object* x_190; lean_object* x_194; lean_object* x_207; uint8_t x_211;
uint8_t x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; uint8_t x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; uint8_t x_97; lean_object* x_98; lean_object* x_99; lean_object* x_100; lean_object* x_101; lean_object* x_108; uint8_t x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113; uint8_t x_114; lean_object* x_115; lean_object* x_116; lean_object* x_117; lean_object* x_120; uint8_t x_121; lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125; lean_object* x_126; lean_object* x_127; uint8_t x_128; lean_object* x_129; lean_object* x_130; lean_object* x_131; uint8_t x_141; lean_object* x_142; lean_object* x_143; lean_object* x_144; lean_object* x_145; lean_object* x_146; lean_object* x_147; uint8_t x_148; lean_object* x_149; lean_object* x_150; lean_object* x_151; lean_object* x_155; lean_object* x_156; lean_object* x_157; lean_object* x_158; lean_object* x_159; lean_object* x_186; lean_object* x_187; lean_object* x_188; lean_object* x_189; lean_object* x_190; lean_object* x_194; lean_object* x_207; uint8_t x_211;
x_20 = 1;
x_211 = lean_unbox(x_17);
if (x_211 == 0)
@ -1992,11 +1992,11 @@ block_49:
{
lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30;
x_26 = l_Lean_Meta_Tactic_TryThis_format_inputWidth;
x_27 = l_Lean_Option_get___at___00Lean_Elab_Term_StructInst_mkMissingFieldsHint_spec__2(x_21, x_26);
lean_dec_ref(x_21);
x_27 = l_Lean_Option_get___at___00Lean_Elab_Term_StructInst_mkMissingFieldsHint_spec__2(x_22, x_26);
lean_dec_ref(x_22);
lean_inc(x_25);
x_28 = lean_apply_1(x_22, x_25);
x_29 = l_Std_Format_pretty(x_24, x_27, x_23, x_28);
x_28 = lean_apply_1(x_21, x_25);
x_29 = l_Std_Format_pretty(x_23, x_27, x_24, x_28);
lean_dec(x_27);
if (x_19 == 0)
{
@ -2069,32 +2069,32 @@ block_63:
lean_object* x_59; lean_object* x_60;
x_59 = lean_alloc_ctor(5, 2, 0);
lean_ctor_set(x_59, 0, x_57);
lean_ctor_set(x_59, 1, x_56);
lean_ctor_set(x_59, 1, x_50);
x_60 = lean_alloc_ctor(5, 2, 0);
lean_ctor_set(x_60, 0, x_59);
lean_ctor_set(x_60, 1, x_58);
if (lean_obj_tag(x_53) == 0)
if (lean_obj_tag(x_55) == 0)
{
if (lean_obj_tag(x_51) == 0)
{
x_21 = x_50;
x_22 = x_52;
x_23 = x_54;
x_24 = x_60;
x_25 = x_55;
x_21 = x_52;
x_22 = x_54;
x_23 = x_60;
x_24 = x_56;
x_25 = x_53;
goto block_49;
}
else
{
lean_object* x_61;
lean_dec(x_55);
lean_dec(x_53);
x_61 = lean_ctor_get(x_51, 0);
lean_inc(x_61);
lean_dec_ref(x_51);
x_21 = x_50;
x_22 = x_52;
x_23 = x_54;
x_24 = x_60;
x_21 = x_52;
x_22 = x_54;
x_23 = x_60;
x_24 = x_56;
x_25 = x_61;
goto block_49;
}
@ -2102,15 +2102,15 @@ goto block_49;
else
{
lean_object* x_62;
lean_dec(x_55);
lean_dec(x_53);
lean_dec(x_51);
x_62 = lean_ctor_get(x_53, 0);
x_62 = lean_ctor_get(x_55, 0);
lean_inc(x_62);
lean_dec_ref(x_53);
x_21 = x_50;
x_22 = x_52;
x_23 = x_54;
x_24 = x_60;
lean_dec_ref(x_55);
x_21 = x_52;
x_22 = x_54;
x_23 = x_60;
x_24 = x_56;
x_25 = x_62;
goto block_49;
}
@ -2123,8 +2123,8 @@ x_72 = lean_box(0);
x_50 = x_64;
x_51 = x_65;
x_52 = x_66;
x_53 = x_67;
x_54 = x_68;
x_53 = x_68;
x_54 = x_67;
x_55 = x_69;
x_56 = x_70;
x_57 = x_71;
@ -2141,8 +2141,8 @@ x_82 = lean_box(0);
x_50 = x_74;
x_51 = x_75;
x_52 = x_76;
x_53 = x_77;
x_54 = x_78;
x_53 = x_78;
x_54 = x_77;
x_55 = x_79;
x_56 = x_80;
x_57 = x_81;
@ -2156,7 +2156,7 @@ x_83 = lean_ctor_get(x_75, 0);
lean_inc_ref(x_76);
lean_inc(x_83);
x_84 = lean_apply_1(x_76, x_83);
x_85 = lean_nat_sub(x_78, x_84);
x_85 = lean_nat_sub(x_80, x_84);
lean_dec(x_84);
x_86 = l_Lean_Elab_Term_StructInst_mkMissingFieldsHint___boxed__const__1;
x_87 = l_List_replicateTR___redArg(x_85, x_86);
@ -2167,8 +2167,8 @@ x_90 = lean_box(0);
x_50 = x_74;
x_51 = x_75;
x_52 = x_76;
x_53 = x_77;
x_54 = x_78;
x_53 = x_78;
x_54 = x_77;
x_55 = x_79;
x_56 = x_80;
x_57 = x_89;
@ -2185,21 +2185,21 @@ if (x_102 == 0)
{
lean_object* x_103; uint8_t x_104;
x_103 = lean_unsigned_to_nat(0u);
x_104 = lean_nat_dec_lt(x_103, x_96);
lean_dec(x_96);
x_104 = lean_nat_dec_lt(x_103, x_98);
lean_dec(x_98);
if (x_104 == 0)
{
if (x_94 == 0)
{
if (x_97 == 0)
{
if (x_92 == 0)
{
lean_object* x_105;
x_105 = ((lean_object*)(l_Lean_Elab_Term_StructInst_mkMissingFieldsHint___closed__5));
x_50 = x_92;
x_50 = x_93;
x_51 = x_101;
x_52 = x_93;
x_53 = x_95;
x_54 = x_98;
x_52 = x_94;
x_53 = x_96;
x_54 = x_95;
x_55 = x_99;
x_56 = x_100;
x_57 = x_105;
@ -2208,11 +2208,11 @@ goto block_63;
}
else
{
x_74 = x_92;
x_74 = x_93;
x_75 = x_101;
x_76 = x_93;
x_76 = x_94;
x_77 = x_95;
x_78 = x_98;
x_78 = x_96;
x_79 = x_99;
x_80 = x_100;
goto block_91;
@ -2220,13 +2220,13 @@ goto block_91;
}
else
{
if (x_97 == 0)
if (x_92 == 0)
{
x_64 = x_92;
x_64 = x_93;
x_65 = x_101;
x_66 = x_93;
x_66 = x_94;
x_67 = x_95;
x_68 = x_98;
x_68 = x_96;
x_69 = x_99;
x_70 = x_100;
goto block_73;
@ -2235,22 +2235,22 @@ else
{
if (x_104 == 0)
{
x_74 = x_92;
x_74 = x_93;
x_75 = x_101;
x_76 = x_93;
x_76 = x_94;
x_77 = x_95;
x_78 = x_98;
x_78 = x_96;
x_79 = x_99;
x_80 = x_100;
goto block_91;
}
else
{
x_64 = x_92;
x_64 = x_93;
x_65 = x_101;
x_66 = x_93;
x_66 = x_94;
x_67 = x_95;
x_68 = x_98;
x_68 = x_96;
x_69 = x_99;
x_70 = x_100;
goto block_73;
@ -2260,11 +2260,11 @@ goto block_73;
}
else
{
x_64 = x_92;
x_64 = x_93;
x_65 = x_101;
x_66 = x_93;
x_66 = x_94;
x_67 = x_95;
x_68 = x_98;
x_68 = x_96;
x_69 = x_99;
x_70 = x_100;
goto block_73;
@ -2273,13 +2273,13 @@ goto block_73;
else
{
lean_object* x_106;
lean_dec(x_96);
lean_dec(x_98);
x_106 = lean_box(0);
x_50 = x_92;
x_50 = x_93;
x_51 = x_101;
x_52 = x_93;
x_53 = x_95;
x_54 = x_98;
x_52 = x_94;
x_53 = x_96;
x_54 = x_95;
x_55 = x_99;
x_56 = x_100;
x_57 = x_106;
@ -2292,13 +2292,13 @@ block_119:
lean_object* x_118;
x_118 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_118, 0, x_117);
x_92 = x_108;
x_93 = x_109;
x_94 = x_111;
x_95 = x_110;
x_96 = x_114;
x_97 = x_113;
x_98 = x_112;
x_92 = x_109;
x_93 = x_108;
x_94 = x_110;
x_95 = x_112;
x_96 = x_111;
x_97 = x_114;
x_98 = x_113;
x_99 = x_115;
x_100 = x_116;
x_101 = x_118;
@ -2323,16 +2323,16 @@ lean_dec(x_136);
if (x_137 == 0)
{
lean_object* x_138;
lean_dec(x_123);
lean_dec(x_121);
lean_dec(x_124);
lean_dec(x_122);
x_138 = lean_box(0);
x_92 = x_120;
x_93 = x_122;
x_94 = x_125;
x_95 = x_124;
x_96 = x_128;
x_97 = x_127;
x_98 = x_126;
x_92 = x_121;
x_93 = x_120;
x_94 = x_123;
x_95 = x_126;
x_96 = x_125;
x_97 = x_128;
x_98 = x_127;
x_99 = x_129;
x_100 = x_130;
x_101 = x_138;
@ -2341,35 +2341,35 @@ goto block_107;
else
{
uint8_t x_139;
x_139 = lean_nat_dec_le(x_121, x_123);
x_139 = lean_nat_dec_le(x_124, x_122);
if (x_139 == 0)
{
lean_dec(x_121);
lean_dec(x_124);
x_108 = x_120;
x_109 = x_122;
x_110 = x_124;
x_109 = x_121;
x_110 = x_123;
x_111 = x_125;
x_112 = x_126;
x_113 = x_127;
x_114 = x_128;
x_115 = x_129;
x_116 = x_130;
x_117 = x_123;
x_117 = x_122;
goto block_119;
}
else
{
lean_dec(x_123);
lean_dec(x_122);
x_108 = x_120;
x_109 = x_122;
x_110 = x_124;
x_109 = x_121;
x_110 = x_123;
x_111 = x_125;
x_112 = x_126;
x_113 = x_127;
x_114 = x_128;
x_115 = x_129;
x_116 = x_130;
x_117 = x_121;
x_117 = x_124;
goto block_119;
}
}
@ -2379,15 +2379,15 @@ block_154:
lean_object* x_152; lean_object* x_153;
x_152 = lean_obj_once(&l_Lean_Elab_Term_StructInst_mkMissingFieldsHint___closed__9, &l_Lean_Elab_Term_StructInst_mkMissingFieldsHint___closed__9_once, _init_l_Lean_Elab_Term_StructInst_mkMissingFieldsHint___closed__9);
x_153 = l_panic___at___00Lean_Elab_Term_StructInst_mkMissingFieldsHint_spec__6(x_152);
x_120 = x_141;
x_121 = x_142;
x_120 = x_142;
x_121 = x_141;
x_122 = x_143;
x_123 = x_144;
x_124 = x_146;
x_125 = x_145;
x_126 = x_149;
x_127 = x_148;
x_128 = x_147;
x_124 = x_145;
x_125 = x_147;
x_126 = x_146;
x_127 = x_149;
x_128 = x_148;
x_129 = x_150;
x_130 = x_151;
x_131 = x_153;
@ -2408,14 +2408,14 @@ lean_inc(x_164);
x_165 = lean_ctor_get(x_9, 6);
lean_inc(x_165);
lean_dec(x_9);
lean_inc_ref(x_157);
x_166 = l_Lean_FileMap_utf8PosToLspPos(x_157, x_163);
lean_inc_ref(x_158);
x_166 = l_Lean_FileMap_utf8PosToLspPos(x_158, x_163);
lean_dec(x_163);
x_167 = lean_ctor_get(x_166, 0);
lean_inc(x_167);
lean_dec_ref(x_166);
lean_inc_ref(x_157);
x_168 = l_Lean_FileMap_utf8PosToLspPos(x_157, x_165);
lean_inc_ref(x_158);
x_168 = l_Lean_FileMap_utf8PosToLspPos(x_158, x_165);
lean_dec(x_165);
x_169 = lean_ctor_get(x_168, 0);
lean_inc(x_169);
@ -2430,9 +2430,9 @@ lean_dec(x_169);
if (x_173 == 0)
{
lean_object* x_174; lean_object* x_175; lean_object* x_176; lean_object* x_177; lean_object* x_178; lean_object* x_179; uint8_t x_180;
x_174 = lean_ctor_get(x_157, 0);
x_174 = lean_ctor_get(x_158, 0);
lean_inc_ref(x_174);
lean_dec_ref(x_157);
lean_dec_ref(x_158);
lean_inc_ref(x_174);
x_175 = l___private_Lean_Elab_StructInstHint_0__Lean_Elab_Term_StructInst_mkMissingFieldsHint_findLineEnd(x_174, x_164);
x_176 = lean_nat_add(x_159, x_171);
@ -2447,17 +2447,17 @@ x_180 = lean_string_is_valid_pos(x_174, x_164);
if (x_180 == 0)
{
lean_dec_ref(x_174);
x_141 = x_155;
x_142 = x_177;
x_143 = x_156;
x_144 = x_179;
x_145 = x_161;
x_146 = x_160;
x_147 = x_162;
x_148 = x_170;
x_149 = x_159;
x_150 = x_164;
x_151 = x_158;
x_141 = x_170;
x_142 = x_155;
x_143 = x_179;
x_144 = x_156;
x_145 = x_177;
x_146 = x_157;
x_147 = x_164;
x_148 = x_161;
x_149 = x_162;
x_150 = x_160;
x_151 = x_159;
goto block_154;
}
else
@ -2467,17 +2467,17 @@ x_181 = lean_string_is_valid_pos(x_174, x_179);
if (x_181 == 0)
{
lean_dec_ref(x_174);
x_141 = x_155;
x_142 = x_177;
x_143 = x_156;
x_144 = x_179;
x_145 = x_161;
x_146 = x_160;
x_147 = x_162;
x_148 = x_170;
x_149 = x_159;
x_150 = x_164;
x_151 = x_158;
x_141 = x_170;
x_142 = x_155;
x_143 = x_179;
x_144 = x_156;
x_145 = x_177;
x_146 = x_157;
x_147 = x_164;
x_148 = x_161;
x_149 = x_162;
x_150 = x_160;
x_151 = x_159;
goto block_154;
}
else
@ -2487,17 +2487,17 @@ x_182 = lean_nat_dec_le(x_164, x_179);
if (x_182 == 0)
{
lean_dec_ref(x_174);
x_141 = x_155;
x_142 = x_177;
x_143 = x_156;
x_144 = x_179;
x_145 = x_161;
x_146 = x_160;
x_147 = x_162;
x_148 = x_170;
x_149 = x_159;
x_150 = x_164;
x_151 = x_158;
x_141 = x_170;
x_142 = x_155;
x_143 = x_179;
x_144 = x_156;
x_145 = x_177;
x_146 = x_157;
x_147 = x_164;
x_148 = x_161;
x_149 = x_162;
x_150 = x_160;
x_151 = x_159;
goto block_154;
}
else
@ -2510,16 +2510,16 @@ lean_ctor_set(x_183, 0, x_174);
lean_ctor_set(x_183, 1, x_164);
lean_ctor_set(x_183, 2, x_179);
x_120 = x_155;
x_121 = x_177;
x_122 = x_156;
x_123 = x_179;
x_124 = x_160;
x_125 = x_161;
x_126 = x_159;
x_127 = x_170;
x_128 = x_162;
x_129 = x_164;
x_130 = x_158;
x_121 = x_170;
x_122 = x_179;
x_123 = x_156;
x_124 = x_177;
x_125 = x_164;
x_126 = x_157;
x_127 = x_162;
x_128 = x_161;
x_129 = x_160;
x_130 = x_159;
x_131 = x_183;
goto block_140;
}
@ -2529,17 +2529,17 @@ goto block_140;
else
{
lean_object* x_184;
lean_dec_ref(x_157);
lean_dec_ref(x_158);
x_184 = lean_box(0);
x_92 = x_155;
x_93 = x_156;
x_94 = x_161;
x_95 = x_160;
x_96 = x_162;
x_97 = x_170;
x_98 = x_159;
x_99 = x_164;
x_100 = x_158;
x_92 = x_170;
x_93 = x_155;
x_94 = x_156;
x_95 = x_157;
x_96 = x_164;
x_97 = x_161;
x_98 = x_162;
x_99 = x_160;
x_100 = x_159;
x_101 = x_184;
goto block_107;
}
@ -2551,9 +2551,9 @@ x_191 = lean_unsigned_to_nat(2u);
x_192 = lean_nat_add(x_190, x_191);
lean_dec(x_190);
x_155 = x_186;
x_156 = x_188;
x_157 = x_187;
x_158 = x_189;
x_156 = x_187;
x_157 = x_189;
x_158 = x_188;
x_159 = x_192;
goto block_185;
}
@ -2576,10 +2576,10 @@ lean_inc_ref(x_195);
x_202 = l_Lean_Elab_Term_StructInst_mkMissingFieldsHint___lam__1(x_195, x_201);
lean_inc_ref(x_195);
lean_inc_ref(x_196);
x_155 = x_196;
x_155 = x_194;
x_156 = x_200;
x_157 = x_195;
x_158 = x_194;
x_157 = x_196;
x_158 = x_195;
x_159 = x_202;
goto block_185;
}
@ -2594,24 +2594,24 @@ x_205 = lean_nat_dec_le(x_203, x_204);
if (x_205 == 0)
{
lean_dec(x_203);
lean_inc_ref(x_195);
lean_inc_ref(x_196);
x_186 = x_196;
x_187 = x_195;
x_188 = x_200;
x_189 = x_194;
lean_inc_ref(x_195);
x_186 = x_194;
x_187 = x_200;
x_188 = x_195;
x_189 = x_196;
x_190 = x_204;
goto block_193;
}
else
{
lean_dec(x_204);
lean_inc_ref(x_195);
lean_inc_ref(x_196);
x_186 = x_196;
x_187 = x_195;
x_188 = x_200;
x_189 = x_194;
lean_inc_ref(x_195);
x_186 = x_194;
x_187 = x_200;
x_188 = x_195;
x_189 = x_196;
x_190 = x_203;
goto block_193;
}

1216
stage0/stdlib/Lean/Language/Lean.c generated
View file

File diff suppressed because it is too large Load diff

5756
stage0/stdlib/Lean/Meta/Tactic/Cbv/ControlFlow.c generated
View file

File diff suppressed because it is too large Load diff

1586
stage0/stdlib/Lean/Parser/Module.c generated
View file

File diff suppressed because it is too large Load diff

2
stage0/stdlib/Lean/Server/FileWorker/RequestHandling.c generated
View file

@ -3331,8 +3331,8 @@ return x_20;
else
{
lean_object* x_39; lean_object* x_40; uint8_t x_41; uint8_t x_47;
lean_dec_ref(x_7);
lean_dec(x_10);
lean_dec_ref(x_7);
lean_del_object(x_8);
x_39 = lean_ctor_get(x_14, 0);
x_47 = !lean_is_exclusive(x_14);

2
stage0/stdlib/Lean/Server/Test/Runner.c generated
View file

@ -1140,7 +1140,7 @@ static const lean_string_object l_Lean_Server_Test_Runner_patchUri___closed__1_v
static const lean_object* l_Lean_Server_Test_Runner_patchUri___closed__1 = (const lean_object*)&l_Lean_Server_Test_Runner_patchUri___closed__1_value;
static const lean_string_object l_Lean_Server_Test_Runner_patchUri___closed__2_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 10, .m_capacity = 10, .m_length = 9, .m_data = "/src/Std/"};
static const lean_object* l_Lean_Server_Test_Runner_patchUri___closed__2 = (const lean_object*)&l_Lean_Server_Test_Runner_patchUri___closed__2_value;
static const lean_string_object l_Lean_Server_Test_Runner_patchUri___closed__3_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 25, .m_capacity = 25, .m_length = 24, .m_data = "/tests/lean/interactive/"};
static const lean_string_object l_Lean_Server_Test_Runner_patchUri___closed__3_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 17, .m_capacity = 17, .m_length = 16, .m_data = "/tests/misc_dir/"};
static const lean_object* l_Lean_Server_Test_Runner_patchUri___closed__3 = (const lean_object*)&l_Lean_Server_Test_Runner_patchUri___closed__3_value;
static const lean_array_object l_Lean_Server_Test_Runner_patchUri___closed__4_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_array_object) + sizeof(void*)*4, .m_other = 0, .m_tag = 246}, .m_size = 4, .m_capacity = 4, .m_data = {((lean_object*)&l_Lean_Server_Test_Runner_patchUri___closed__0_value),((lean_object*)&l_Lean_Server_Test_Runner_patchUri___closed__1_value),((lean_object*)&l_Lean_Server_Test_Runner_patchUri___closed__2_value),((lean_object*)&l_Lean_Server_Test_Runner_patchUri___closed__3_value)}};
static const lean_object* l_Lean_Server_Test_Runner_patchUri___closed__4 = (const lean_object*)&l_Lean_Server_Test_Runner_patchUri___closed__4_value;