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:
Leonardo de Moura 2022-02-25 16:32:03 -08:00
parent 77dda12bc9
commit cd710e903e
18 changed files with 5020 additions and 1651 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
stage0/src/Init/Core.lean generated
View file

@ -176,6 +176,24 @@ theorem optParam_eq (α : Sort u) (default : α) : optParam α default = α := r
infix:50 " != " => bne
class LawfulBEq (α : Type u) [BEq α] : Prop where
eq_of_beq : (a b : α) → (a == b) = true → a = b
theorem eq_of_beq [BEq α] [LawfulBEq α] {a b : α} (h : (a == b) = true) : a = b :=
LawfulBEq.eq_of_beq a b h
instance : LawfulBEq Bool where
eq_of_beq a b h := by cases a <;> cases b <;> first | rfl | contradiction
instance : LawfulBEq Nat where
eq_of_beq _ _ h := of_decide_eq_true h
instance : LawfulBEq Char where
eq_of_beq _ _ h := of_decide_eq_true h
instance : LawfulBEq String where
eq_of_beq _ _ h := of_decide_eq_true h
/- Logical connectives an equality -/
def implies (a b : Prop) := a → b

1
stage0/src/Init/Data.lean generated
View file

@ -25,3 +25,4 @@ import Init.Data.Hashable
import Init.Data.OfScientific
import Init.Data.Format
import Init.Data.Stream
import Init.Data.Prod

12
stage0/src/Init/Data/List/Basic.lean generated
View file

@ -472,4 +472,16 @@ def minimum? [LE α] [DecidableRel (@LE.le α _)] : List α → Option α
| [] => none
| a::as => some <| as.foldl min a
instance [BEq α] [LawfulBEq α] : LawfulBEq (List α) where
eq_of_beq as bs := by
induction as generalizing bs with
| nil => intro h; cases bs <;> first | rfl | contradiction
| cons a as ih =>
cases bs with
| nil => intro h; contradiction
| cons b bs =>
simp [BEq.beq, List.beq]
intro ⟨h₁, h₂⟩
exact ⟨eq_of_beq h₁, ih _ h₂⟩
end List

97
stage0/src/Init/Data/Nat/Linear.lean generated
View file

@ -9,6 +9,7 @@ import Init.Classical
import Init.SimpLemmas
import Init.Data.Nat.Basic
import Init.Data.List.Basic
import Init.Data.Prod
namespace Nat.Linear
@ -146,6 +147,17 @@ structure PolyCnstr where
eq : Bool
lhs : Poly
rhs : Poly
deriving BEq
-- TODO: implement LawfulBEq generator companion for BEq
instance : LawfulBEq PolyCnstr where
eq_of_beq a b h := by
cases a; rename_i eq₁ lhs₁ rhs₁
cases b; rename_i eq₂ lhs₂ rhs₂
have h : eq₁ == eq₂ && lhs₁ == lhs₂ && rhs₁ == rhs₂ := h
simp at h
have ⟨⟨h₁, h₂⟩, h₃⟩ := h
rw [h₁, eq_of_beq h₂, eq_of_beq h₃]
def PolyCnstr.mul (k : Nat) (c : PolyCnstr) : PolyCnstr :=
{ c with lhs := c.lhs.mul k, rhs := c.rhs.mul k }
@ -181,6 +193,10 @@ def PolyCnstr.isValid (c : PolyCnstr) : Bool :=
else
c.lhs.isZero
/-- Return true iff `c₁` has fewer monomials than `c₂`. -/
def PolyCnstr.hasFewerMonomials (c₁ c₂ : PolyCnstr) : Bool :=
c₁.lhs.length + c₁.rhs.length < c₂.lhs.length + c₂.rhs.length
def ExprCnstr.denote (ctx : Context) (c : ExprCnstr) : Prop :=
if c.eq then
c.lhs.denote ctx = c.rhs.denote ctx
@ -188,6 +204,9 @@ def ExprCnstr.denote (ctx : Context) (c : ExprCnstr) : Prop :=
c.lhs.denote ctx ≤ c.rhs.denote ctx
def ExprCnstr.toPoly (c : ExprCnstr) : PolyCnstr :=
{ c with lhs := c.lhs.toPoly, rhs := c.rhs.toPoly }
def ExprCnstr.toNormPoly (c : ExprCnstr) : PolyCnstr :=
let (lhs, rhs) := Poly.cancel c.lhs.toNormPoly c.rhs.toNormPoly
{ c with lhs, rhs }
@ -196,18 +215,39 @@ abbrev Certificate := List (Nat × ExprCnstr)
def Certificate.combineHyps (c : PolyCnstr) (hs : Certificate) : PolyCnstr :=
match hs with
| [] => c
| (k, c') :: hs => combineHyps (PolyCnstr.combine c (c'.toPoly.mul (k+1))) hs
| (k, c') :: hs => combineHyps (PolyCnstr.combine c (c'.toNormPoly.mul (k+1))) hs
def Certificate.combine (hs : Certificate) : PolyCnstr :=
match hs with
| [] => { eq := true, lhs := [], rhs := [] }
| (k, c) :: hs => combineHyps (c.toPoly.mul (k+1)) hs
| (k, c) :: hs => combineHyps (c.toNormPoly.mul (k+1)) hs
def Certificate.denote (ctx : Context) (c : Certificate) : Prop :=
match c with
| [] => False
| (_, c)::hs => c.denote ctx → denote ctx hs
def monomialToExpr (k : Nat) (v : Var) : Expr :=
if v = fixedVar then
Expr.num k
else if k = 1 then
Expr.var v
else
Expr.mulL k (Expr.var v)
def Poly.toExpr (p : Poly) : Expr :=
match p with
| [] => Expr.num 0
| (k, v) :: p => go (monomialToExpr k v) p
where
go (e : Expr) (p : Poly) : Expr :=
match p with
| [] => e
| (k, v) :: p => go (Expr.add e (monomialToExpr k v)) p
def PolyCnstr.toExpr (c : PolyCnstr) : ExprCnstr :=
{ c with lhs := c.lhs.toExpr, rhs := c.rhs.toExpr }
attribute [local simp] Nat.add_comm Nat.add_assoc Nat.add_left_comm Nat.right_distrib Nat.left_distrib Nat.mul_assoc Nat.mul_comm
attribute [local simp] Poly.denote Expr.denote Poly.insertSorted Poly.sort Poly.sort.go Poly.fuse Poly.cancelAux
attribute [local simp] Poly.mul Poly.mul.go
@ -439,7 +479,7 @@ theorem Poly.denote_le_cancel_eq (ctx : Context) (m₁ m₂ : Poly) : denote_le
attribute [local simp] Poly.denote_le_cancel_eq
@[simp] theorem Expr.denote_toPoly (ctx : Context) (e : Expr) : e.toPoly.denote ctx = e.denote ctx := by
theorem Expr.denote_toPoly (ctx : Context) (e : Expr) : e.toPoly.denote ctx = e.denote ctx := by
induction e with
| num k => by_cases h : k = 0 <;> simp [toPoly, h, Var.denote]
| var i => simp [toPoly]
@ -447,6 +487,8 @@ attribute [local simp] Poly.denote_le_cancel_eq
| mulL k a ih => simp [toPoly, ih, -Poly.mul]
| mulR k a ih => simp [toPoly, ih, -Poly.mul]
attribute [local simp] Expr.denote_toPoly
theorem Expr.eq_of_toNormPoly (ctx : Context) (a b : Expr) (h : a.toNormPoly = b.toNormPoly) : a.denote ctx = b.denote ctx := by
simp [toNormPoly] at h
have h := congrArg (Poly.denote ctx) h
@ -468,14 +510,26 @@ theorem Expr.of_cancel_le (ctx : Context) (a b c d : Expr) (h : Poly.cancel a.to
theorem Expr.of_cancel_lt (ctx : Context) (a b c d : Expr) (h : Poly.cancel a.inc.toNormPoly b.toNormPoly = (c.inc.toPoly, d.toPoly)) : (a.denote ctx < b.denote ctx) = (c.denote ctx < d.denote ctx) :=
of_cancel_le ctx a.inc b c.inc d h
theorem ExprCnstr.toPoly_norm_eq (c : ExprCnstr) : c.toPoly.norm = c.toNormPoly :=
rfl
theorem ExprCnstr.denote_toPoly (ctx : Context) (c : ExprCnstr) : c.toPoly.denote ctx = c.denote ctx := by
cases c; rename_i eq lhs rhs
simp [ExprCnstr.denote, PolyCnstr.denote, ExprCnstr.toPoly]
simp [ExprCnstr.denote, PolyCnstr.denote, ExprCnstr.toPoly];
by_cases h : eq = true <;> simp [h]
. simp [Poly.denote_eq, Expr.toPoly]
. simp [Poly.denote_le, Expr.toPoly]
attribute [local simp] ExprCnstr.denote_toPoly
theorem ExprCnstr.denote_toNormPoly (ctx : Context) (c : ExprCnstr) : c.toNormPoly.denote ctx = c.denote ctx := by
cases c; rename_i eq lhs rhs
simp [ExprCnstr.denote, PolyCnstr.denote, ExprCnstr.toNormPoly]
by_cases h : eq = true <;> simp [h]
. rw [Poly.denote_eq_cancel_eq]; simp [Poly.denote_eq, Expr.toNormPoly]
. rw [Poly.denote_le_cancel_eq]; simp [Poly.denote_le, Expr.toNormPoly]
attribute [local simp] ExprCnstr.denote_toPoly
attribute [local simp] ExprCnstr.denote_toNormPoly
theorem Poly.mul.go_denote (ctx : Context) (k : Nat) (p : Poly) : (Poly.mul.go k p).denote ctx = k * p.denote ctx := by
match p with
@ -558,12 +612,12 @@ def PolyCnstr.eq_true_of_isValid (ctx : Context) {c : PolyCnstr} : c.isValid →
have := Nat.zero_le (Poly.denote ctx rhs)
simp [this]
def ExprCnstr.eq_false_of_isUnsat (ctx : Context) (c : ExprCnstr) (h : c.toPoly.isUnsat) : c.denote ctx = False := by
def ExprCnstr.eq_false_of_isUnsat (ctx : Context) (c : ExprCnstr) (h : c.toNormPoly.isUnsat) : c.denote ctx = False := by
have := PolyCnstr.eq_false_of_isUnsat ctx h
simp at this
assumption
def ExprCnstr.eq_true_of_isValid (ctx : Context) (c : ExprCnstr) (h : c.toPoly.isValid) : c.denote ctx = True := by
def ExprCnstr.eq_true_of_isValid (ctx : Context) (c : ExprCnstr) (h : c.toNormPoly.isValid) : c.denote ctx = True := by
have := PolyCnstr.eq_true_of_isValid ctx h
simp at this
assumption
@ -573,10 +627,10 @@ theorem Certificate.of_combineHyps (ctx : Context) (c : PolyCnstr) (cs : Certifi
| [] => simp [combineHyps, denote] at *; exact h
| (k, c')::cs =>
intro h₁ h₂
have := PolyCnstr.denote_combine (ctx := ctx) (c₂ := PolyCnstr.mul (k + 1) (ExprCnstr.toPoly c')) h₁
have := PolyCnstr.denote_combine (ctx := ctx) (c₂ := PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c')) h₁
simp at this
have := this h₂
have ih := of_combineHyps ctx (PolyCnstr.combine c (PolyCnstr.mul (k + 1) (ExprCnstr.toPoly c'))) cs
have ih := of_combineHyps ctx (PolyCnstr.combine c (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c'))) cs
exact ih h this
theorem Certificate.of_combine (ctx : Context) (cs : Certificate) (h : cs.combine.denote ctx → False) : cs.denote ctx := by
@ -592,4 +646,29 @@ theorem Certificate.of_combine_isUnsat (ctx : Context) (cs : Certificate) (h : c
have h := PolyCnstr.eq_false_of_isUnsat ctx h
of_combine ctx cs (fun h' => Eq.mp h h')
theorem denote_monomialToExpr (ctx : Context) (k : Nat) (v : Var) : (monomialToExpr k v).denote ctx = k * v.denote ctx := by
simp [monomialToExpr]
by_cases h : v = fixedVar <;> simp [h, Expr.denote]
. simp [Var.denote]
. by_cases h : k = 1 <;> simp [h, Expr.denote]
attribute [local simp] denote_monomialToExpr
theorem Poly.denote_toExpr_go (ctx : Context) (e : Expr) (p : Poly) : (toExpr.go e p).denote ctx = e.denote ctx + p.denote ctx := by
induction p generalizing e with
| nil => simp [toExpr.go, Poly.denote]
| cons kv p ih => cases kv; simp [toExpr.go, ih, Expr.denote, Poly.denote]
attribute [local simp] Poly.denote_toExpr_go
theorem Poly.denote_toExpr (ctx : Context) (p : Poly) : p.toExpr.denote ctx = p.denote ctx := by
match p with
| [] => simp [toExpr, Expr.denote, Poly.denote]
| (k, v) :: p => simp [toExpr, Expr.denote, Poly.denote]
theorem ExprCnstr.eq_of_toNormPoly_eq (ctx : Context) (c d : ExprCnstr) (h : c.toNormPoly == d.toPoly) : c.denote ctx = d.denote ctx := by
have h := congrArg (PolyCnstr.denote ctx) (eq_of_beq h)
simp at h
assumption
end Nat.Linear

10
stage0/src/Init/Data/Prod.lean generated Normal file
View file

@ -0,0 +1,10 @@
/-
Copyright (c) 2022 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
-/
prelude
import Init.SimpLemmas
instance [BEq α] [BEq β] [LawfulBEq α] [LawfulBEq β] : LawfulBEq (α × β) where
eq_of_beq a b h := by cases a; cases b; simp [BEq.beq] at h; have ⟨h₁, h₂⟩ := h; rw [eq_of_beq h₁, eq_of_beq h₂]

4
stage0/src/Init/Meta.lean generated
View file

@ -1008,6 +1008,7 @@ structure Config where
iota : Bool := true
proj : Bool := true
decide : Bool := true
arith : Bool := true
deriving Inhabited, BEq, Repr
-- Configuration object for `simp_all`
@ -1020,7 +1021,8 @@ def neutralConfig : Simp.Config :=
eta := false
iota := false
proj := false
decide := false }
decide := false
arith := false }
end Simp

1
stage0/src/Lean/Meta/Tactic/LinearArith.lean generated
View file

@ -4,3 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich
-/
import Lean.Meta.Tactic.LinearArith.Basic
import Lean.Meta.Tactic.LinearArith.Nat

76
stage0/src/Lean/Meta/Tactic/LinearArith/Nat.lean generated
View file

@ -12,25 +12,48 @@ deriving instance Repr for Nat.Linear.Expr
abbrev LinearExpr := Nat.Linear.Expr
abbrev LinearCnstr := Nat.Linear.ExprCnstr
abbrev PolyExpr := Nat.Linear.Poly
def LinearExpr.toExpr (ctx : Array Expr) (e : LinearExpr) : Expr :=
def LinearExpr.toExpr (e : LinearExpr) : Expr :=
open Nat.Linear.Expr in
match e with
| num v => mkApp (mkConst ``num) (mkNatLit v)
| var i => if h : i < ctx.size then ctx.get ⟨i, h⟩ else mkApp (mkConst ``var) (mkNatLit i)
| add a b => mkApp2 (mkConst ``add) (toExpr ctx a) (toExpr ctx b)
| mulL k a => mkApp2 (mkConst ``mulL) (mkNatLit k) (toExpr ctx a)
| mulR a k => mkApp2 (mkConst ``mulL) (toExpr ctx a) (mkNatLit k)
| var i => mkApp (mkConst ``var) (mkNatLit i)
| add a b => mkApp2 (mkConst ``add) (toExpr a) (toExpr b)
| mulL k a => mkApp2 (mkConst ``mulL) (mkNatLit k) (toExpr a)
| mulR a k => mkApp2 (mkConst ``mulL) (toExpr a) (mkNatLit k)
instance : ToExpr LinearExpr where
toExpr a := a.toExpr #[]
toExpr a := a.toExpr
toTypeExpr := mkConst ``Nat.Linear.Expr
protected def LinearCnstr.toExpr (c : LinearCnstr) : Expr :=
mkApp3 (mkConst ``Nat.Linear.ExprCnstr.mk) (toExpr c.eq) (LinearExpr.toExpr c.lhs) (LinearExpr.toExpr c.rhs)
instance : ToExpr LinearCnstr where
toExpr a := a.toExpr
toTypeExpr := mkConst ``Nat.Linear.ExprCnstr
open Nat.Linear.Expr in
def LinearExpr.toArith (ctx : Array Expr) (e : LinearExpr) : MetaM Expr := do
match e with
| num v => return mkNatLit v
| var i => return ctx[i]
| add a b => mkAdd (← toArith ctx a) (← toArith ctx b)
| mulL k a => mkMul (mkNatLit k) (← toArith ctx a)
| mulR a k => mkMul (← toArith ctx a) (mkNatLit k)
def LinearCnstr.toArith (ctx : Array Expr) (c : LinearCnstr) : MetaM Expr := do
if c.eq then
mkEq (← LinearExpr.toArith ctx c.lhs) (← LinearExpr.toArith ctx c.rhs)
else
return mkApp4 (mkConst ``LE.le [levelZero]) (mkConst ``Nat) (mkConst ``instLENat) (← LinearExpr.toArith ctx c.lhs) (← LinearExpr.toArith ctx c.rhs)
namespace ToLinear
structure State where
varMap : ExprMap Nat
vars : Array Expr
varMap : ExprMap Nat := {}
vars : Array Expr := #[]
abbrev M := StateRefT State MetaM
@ -101,14 +124,47 @@ partial def toLinearCnstr? (e : Expr) : M (Option LinearCnstr) := do
else if declName == ``Nat.lt && numArgs == 2 then
return some { eq := false, lhs := (← toLinearExpr (e.getArg! 0)).inc, rhs := (← toLinearExpr (e.getArg! 1)) }
else if numArgs == 4 && (declName == ``LE.le || declName == ``GE.ge || declName == ``LT.lt || declName == ``GT.gt) then
if let some e ← unfoldProjInst? e then
toLinearCnstr? e
if (← isDefEq (e.getArg! 0) (mkConst ``Nat)) then
if let some e ← unfoldProjInst? e then
toLinearCnstr? e
else
return none
else
return none
else
return none
| _ => return none
def run (x : M α) : MetaM (α × Array Expr) := do
let (a, s) ← x.run {}
return (a, s.vars)
end ToLinear
open ToLinear (toLinearCnstr? toLinearExpr)
def toContextExpr (ctx : Array Expr) : MetaM Expr := do
mkListLit (mkConst ``Nat) ctx.toList
def reflTrue : Expr :=
mkApp2 (mkConst ``Eq.refl [levelOne]) (mkConst ``Bool) (mkConst ``Bool.true)
def simpCnstr? (e : Expr) : MetaM (Option (Expr × Expr)) := do
let (some c, ctx) ← ToLinear.run (ToLinear.toLinearCnstr? e) | return none
let c₁ := c.toPoly
let c₂ := c₁.norm
if c₂.isUnsat then
let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_false_of_isUnsat) (← toContextExpr ctx) (toExpr c) reflTrue
return some (mkConst ``False, p)
else if c₂.isValid then
let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_true_of_isValid) (← toContextExpr ctx) (toExpr c) reflTrue
return some (mkConst ``True, p)
else if c₂.hasFewerMonomials c₁ then
let c₂ : LinearCnstr := c₂.toExpr
let p := mkApp4 (mkConst ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq) (← toContextExpr ctx) (toExpr c) (toExpr c₂) reflTrue
let r ← c₂.toArith ctx
return some (r, p)
else
return none
end Lean.Meta.Linear.Nat

6
stage0/stdlib/Init/Data.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Data
// Imports: Init.Data.Basic Init.Data.Nat Init.Data.Char Init.Data.String Init.Data.List Init.Data.Int Init.Data.Array Init.Data.ByteArray Init.Data.FloatArray Init.Data.Fin Init.Data.UInt Init.Data.Float Init.Data.Option Init.Data.Ord Init.Data.Random Init.Data.ToString Init.Data.Range Init.Data.Hashable Init.Data.OfScientific Init.Data.Format Init.Data.Stream
// Imports: Init.Data.Basic Init.Data.Nat Init.Data.Char Init.Data.String Init.Data.List Init.Data.Int Init.Data.Array Init.Data.ByteArray Init.Data.FloatArray Init.Data.Fin Init.Data.UInt Init.Data.Float Init.Data.Option Init.Data.Ord Init.Data.Random Init.Data.ToString Init.Data.Range Init.Data.Hashable Init.Data.OfScientific Init.Data.Format Init.Data.Stream Init.Data.Prod
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -34,6 +34,7 @@ lean_object* initialize_Init_Data_Hashable(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_OfScientific(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_Format(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_Stream(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_Prod(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Init_Data(uint8_t builtin, lean_object* w) {
lean_object * res;
@ -102,6 +103,9 @@ lean_dec_ref(res);
res = initialize_Init_Data_Stream(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Prod(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

385
stage0/stdlib/Init/Data/Nat/Linear.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Data.Nat.Linear
// Imports: Init.Coe Init.Classical Init.SimpLemmas Init.Data.Nat.Basic Init.Data.List.Basic
// Imports: Init.Coe Init.Classical Init.SimpLemmas Init.Data.Nat.Basic Init.Data.List.Basic Init.Data.Prod
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -15,10 +15,12 @@ extern "C" {
#endif
lean_object* l_List_reverse___rarg(lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_ExprCnstr_toPoly(lean_object*);
LEAN_EXPORT uint8_t l_List_beq___at___private_Init_Data_Nat_Linear_0__Nat_Linear_beqPolyCnstr____x40_Init_Data_Nat_Linear___hyg_1258____spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_Poly_mul_go(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_PolyCnstr_norm(lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_Poly_cancelAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_Certificate_combine___boxed(lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_Nat_Linear_0__Nat_Linear_beqPolyCnstr____x40_Init_Data_Nat_Linear___hyg_1258____boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_fixedVar;
LEAN_EXPORT lean_object* l_Nat_Linear_Poly_cancel(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_Poly_sort_go(lean_object*, lean_object*);
@ -28,10 +30,12 @@ LEAN_EXPORT lean_object* l_Nat_Linear_Poly_denote___boxed(lean_object*, lean_obj
LEAN_EXPORT lean_object* l_Nat_Linear_Expr_toPoly(lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_Certificate_combineHyps___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_Expr_toNormPoly___boxed(lean_object*);
LEAN_EXPORT uint8_t l_Nat_Linear_PolyCnstr_hasFewerMonomials(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_Expr_denote___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_PolyCnstr_mul___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_Var_denote_go___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_Poly_mul___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_monomialToExpr(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Nat_Linear_Poly_isZero(lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_Certificate_combine(lean_object*);
@ -40,18 +44,26 @@ LEAN_EXPORT lean_object* l_Nat_Linear_Poly_sort(lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_Expr_denote(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_Poly_toExpr_go(lean_object*, lean_object*);
static lean_object* l_Nat_Linear_instInhabitedExpr___closed__1;
LEAN_EXPORT lean_object* l_Nat_Linear_PolyCnstr_toExpr(lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_Poly_isZero___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_Expr_inc(lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_Poly_mul(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_Var_denote_go(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_Poly_denote(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_instBEqPolyCnstr;
LEAN_EXPORT uint8_t l_Nat_Linear_PolyCnstr_isValid(lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_PolyCnstr_isUnsat___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_PolyCnstr_mul(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_beq___at___private_Init_Data_Nat_Linear_0__Nat_Linear_beqPolyCnstr____x40_Init_Data_Nat_Linear___hyg_1258____spec__1___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_ExprCnstr_toNormPoly(lean_object*);
LEAN_EXPORT uint8_t l___private_Init_Data_Nat_Linear_0__Nat_Linear_beqPolyCnstr____x40_Init_Data_Nat_Linear___hyg_1258_(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_Poly_toExpr(lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_Expr_toNormPoly(lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_Expr_toPoly___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_instInhabitedExpr;
LEAN_EXPORT lean_object* l_Nat_Linear_ExprCnstr_toNormPoly___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_Poly_isNum_x3f___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_Certificate_combineHyps(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Nat_Linear_Poly_isNonZero(lean_object*);
@ -67,6 +79,8 @@ static lean_object* l_Nat_Linear_Expr_inc___closed__1;
LEAN_EXPORT lean_object* l_Nat_Linear_PolyCnstr_combine(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Nat_Linear_PolyCnstr_isUnsat(lean_object*);
lean_object* l_List_appendTR___rarg(lean_object*, lean_object*);
static lean_object* l_Nat_Linear_instBEqPolyCnstr___closed__1;
LEAN_EXPORT lean_object* l_Nat_Linear_PolyCnstr_hasFewerMonomials___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_PolyCnstr_isValid___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_Poly_fuse(lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
@ -2171,6 +2185,181 @@ lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
LEAN_EXPORT uint8_t l_List_beq___at___private_Init_Data_Nat_Linear_0__Nat_Linear_beqPolyCnstr____x40_Init_Data_Nat_Linear___hyg_1258____spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
if (lean_obj_tag(x_2) == 0)
{
uint8_t x_3;
x_3 = 1;
return x_3;
}
else
{
uint8_t x_4;
x_4 = 0;
return x_4;
}
}
else
{
if (lean_obj_tag(x_2) == 0)
{
uint8_t x_5;
x_5 = 0;
return x_5;
}
else
{
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; uint8_t x_14;
x_6 = lean_ctor_get(x_1, 0);
x_7 = lean_ctor_get(x_2, 0);
x_8 = lean_ctor_get(x_1, 1);
x_9 = lean_ctor_get(x_2, 1);
x_10 = lean_ctor_get(x_6, 0);
x_11 = lean_ctor_get(x_6, 1);
x_12 = lean_ctor_get(x_7, 0);
x_13 = lean_ctor_get(x_7, 1);
x_14 = lean_nat_dec_eq(x_10, x_12);
if (x_14 == 0)
{
uint8_t x_15;
x_15 = 0;
return x_15;
}
else
{
uint8_t x_16;
x_16 = lean_nat_dec_eq(x_11, x_13);
if (x_16 == 0)
{
uint8_t x_17;
x_17 = 0;
return x_17;
}
else
{
x_1 = x_8;
x_2 = x_9;
goto _start;
}
}
}
}
}
}
LEAN_EXPORT uint8_t l___private_Init_Data_Nat_Linear_0__Nat_Linear_beqPolyCnstr____x40_Init_Data_Nat_Linear___hyg_1258_(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4; lean_object* x_5; uint8_t x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9;
x_3 = lean_ctor_get_uint8(x_1, sizeof(void*)*2);
x_4 = lean_ctor_get(x_1, 0);
x_5 = lean_ctor_get(x_1, 1);
x_6 = lean_ctor_get_uint8(x_2, sizeof(void*)*2);
x_7 = lean_ctor_get(x_2, 0);
x_8 = lean_ctor_get(x_2, 1);
if (x_3 == 0)
{
if (x_6 == 0)
{
uint8_t x_15;
x_15 = 1;
x_9 = x_15;
goto block_14;
}
else
{
uint8_t x_16;
x_16 = 0;
x_9 = x_16;
goto block_14;
}
}
else
{
if (x_6 == 0)
{
uint8_t x_17;
x_17 = 0;
x_9 = x_17;
goto block_14;
}
else
{
uint8_t x_18;
x_18 = 1;
x_9 = x_18;
goto block_14;
}
}
block_14:
{
if (x_9 == 0)
{
uint8_t x_10;
x_10 = 0;
return x_10;
}
else
{
uint8_t x_11;
x_11 = l_List_beq___at___private_Init_Data_Nat_Linear_0__Nat_Linear_beqPolyCnstr____x40_Init_Data_Nat_Linear___hyg_1258____spec__1(x_4, x_7);
if (x_11 == 0)
{
uint8_t x_12;
x_12 = 0;
return x_12;
}
else
{
uint8_t x_13;
x_13 = l_List_beq___at___private_Init_Data_Nat_Linear_0__Nat_Linear_beqPolyCnstr____x40_Init_Data_Nat_Linear___hyg_1258____spec__1(x_5, x_8);
return x_13;
}
}
}
}
}
LEAN_EXPORT lean_object* l_List_beq___at___private_Init_Data_Nat_Linear_0__Nat_Linear_beqPolyCnstr____x40_Init_Data_Nat_Linear___hyg_1258____spec__1___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l_List_beq___at___private_Init_Data_Nat_Linear_0__Nat_Linear_beqPolyCnstr____x40_Init_Data_Nat_Linear___hyg_1258____spec__1(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
}
}
LEAN_EXPORT lean_object* l___private_Init_Data_Nat_Linear_0__Nat_Linear_beqPolyCnstr____x40_Init_Data_Nat_Linear___hyg_1258____boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l___private_Init_Data_Nat_Linear_0__Nat_Linear_beqPolyCnstr____x40_Init_Data_Nat_Linear___hyg_1258_(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
}
}
static lean_object* _init_l_Nat_Linear_instBEqPolyCnstr___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Init_Data_Nat_Linear_0__Nat_Linear_beqPolyCnstr____x40_Init_Data_Nat_Linear___hyg_1258____boxed), 2, 0);
return x_1;
}
}
static lean_object* _init_l_Nat_Linear_instBEqPolyCnstr() {
_start:
{
lean_object* x_1;
x_1 = l_Nat_Linear_instBEqPolyCnstr___closed__1;
return x_1;
}
}
LEAN_EXPORT lean_object* l_Nat_Linear_PolyCnstr_mul(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -2500,9 +2689,70 @@ x_3 = lean_box(x_2);
return x_3;
}
}
LEAN_EXPORT uint8_t l_Nat_Linear_PolyCnstr_hasFewerMonomials(lean_object* x_1, lean_object* x_2) {
_start:
{
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; uint8_t x_14;
x_3 = lean_ctor_get(x_1, 0);
x_4 = lean_unsigned_to_nat(0u);
x_5 = l_List_lengthTRAux___rarg(x_3, x_4);
x_6 = lean_ctor_get(x_1, 1);
x_7 = l_List_lengthTRAux___rarg(x_6, x_4);
x_8 = lean_nat_add(x_5, x_7);
lean_dec(x_7);
lean_dec(x_5);
x_9 = lean_ctor_get(x_2, 0);
x_10 = l_List_lengthTRAux___rarg(x_9, x_4);
x_11 = lean_ctor_get(x_2, 1);
x_12 = l_List_lengthTRAux___rarg(x_11, x_4);
x_13 = lean_nat_add(x_10, x_12);
lean_dec(x_12);
lean_dec(x_10);
x_14 = lean_nat_dec_lt(x_8, x_13);
lean_dec(x_13);
lean_dec(x_8);
return x_14;
}
}
LEAN_EXPORT lean_object* l_Nat_Linear_PolyCnstr_hasFewerMonomials___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l_Nat_Linear_PolyCnstr_hasFewerMonomials(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Nat_Linear_ExprCnstr_toPoly(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = lean_ctor_get_uint8(x_1, sizeof(void*)*2);
x_3 = lean_ctor_get(x_1, 0);
x_4 = lean_ctor_get(x_1, 1);
x_5 = l_Nat_Linear_Expr_toPoly(x_3);
x_6 = l_Nat_Linear_Expr_toPoly(x_4);
x_7 = lean_alloc_ctor(0, 2, 1);
lean_ctor_set(x_7, 0, x_5);
lean_ctor_set(x_7, 1, x_6);
lean_ctor_set_uint8(x_7, sizeof(void*)*2, x_2);
return x_7;
}
}
LEAN_EXPORT lean_object* l_Nat_Linear_ExprCnstr_toPoly___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Nat_Linear_ExprCnstr_toPoly(x_1);
lean_dec(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Nat_Linear_ExprCnstr_toNormPoly(lean_object* x_1) {
_start:
{
uint8_t 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;
x_2 = lean_ctor_get_uint8(x_1, sizeof(void*)*2);
x_3 = lean_ctor_get(x_1, 0);
@ -2522,11 +2772,11 @@ lean_ctor_set_uint8(x_10, sizeof(void*)*2, x_2);
return x_10;
}
}
LEAN_EXPORT lean_object* l_Nat_Linear_ExprCnstr_toPoly___boxed(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Nat_Linear_ExprCnstr_toNormPoly___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Nat_Linear_ExprCnstr_toPoly(x_1);
x_2 = l_Nat_Linear_ExprCnstr_toNormPoly(x_1);
lean_dec(x_1);
return x_2;
}
@ -2547,7 +2797,7 @@ x_5 = lean_ctor_get(x_3, 0);
x_6 = lean_ctor_get(x_3, 1);
x_7 = lean_unsigned_to_nat(1u);
x_8 = lean_nat_add(x_5, x_7);
x_9 = l_Nat_Linear_ExprCnstr_toPoly(x_6);
x_9 = l_Nat_Linear_ExprCnstr_toNormPoly(x_6);
x_10 = l_Nat_Linear_PolyCnstr_mul(x_8, x_9);
lean_dec(x_8);
x_11 = l_Nat_Linear_PolyCnstr_combine(x_1, x_10);
@ -2597,7 +2847,7 @@ x_5 = lean_ctor_get(x_3, 0);
x_6 = lean_ctor_get(x_3, 1);
x_7 = lean_unsigned_to_nat(1u);
x_8 = lean_nat_add(x_5, x_7);
x_9 = l_Nat_Linear_ExprCnstr_toPoly(x_6);
x_9 = l_Nat_Linear_ExprCnstr_toNormPoly(x_6);
x_10 = l_Nat_Linear_PolyCnstr_mul(x_8, x_9);
lean_dec(x_8);
x_11 = l_Nat_Linear_Certificate_combineHyps(x_10, x_4);
@ -2614,11 +2864,129 @@ lean_dec(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Nat_Linear_monomialToExpr(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; uint8_t x_4;
x_3 = l_Nat_Linear_fixedVar;
x_4 = lean_nat_dec_eq(x_2, x_3);
if (x_4 == 0)
{
lean_object* x_5; uint8_t x_6;
x_5 = lean_unsigned_to_nat(1u);
x_6 = lean_nat_dec_eq(x_1, x_5);
if (x_6 == 0)
{
lean_object* x_7; lean_object* x_8;
x_7 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_7, 0, x_2);
x_8 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_8, 0, x_1);
lean_ctor_set(x_8, 1, x_7);
return x_8;
}
else
{
lean_object* x_9;
lean_dec(x_1);
x_9 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_9, 0, x_2);
return x_9;
}
}
else
{
lean_object* x_10;
lean_dec(x_2);
x_10 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_10, 0, x_1);
return x_10;
}
}
}
LEAN_EXPORT lean_object* l_Nat_Linear_Poly_toExpr_go(lean_object* x_1, lean_object* x_2) {
_start:
{
if (lean_obj_tag(x_2) == 0)
{
return x_1;
}
else
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
x_4 = lean_ctor_get(x_2, 1);
lean_inc(x_4);
lean_dec(x_2);
x_5 = lean_ctor_get(x_3, 0);
lean_inc(x_5);
x_6 = lean_ctor_get(x_3, 1);
lean_inc(x_6);
lean_dec(x_3);
x_7 = l_Nat_Linear_monomialToExpr(x_5, x_6);
x_8 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_8, 0, x_1);
lean_ctor_set(x_8, 1, x_7);
x_1 = x_8;
x_2 = x_4;
goto _start;
}
}
}
LEAN_EXPORT lean_object* l_Nat_Linear_Poly_toExpr(lean_object* x_1) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
lean_object* x_2;
x_2 = l_Nat_Linear_instInhabitedExpr___closed__1;
return x_2;
}
else
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_3 = lean_ctor_get(x_1, 0);
lean_inc(x_3);
x_4 = lean_ctor_get(x_1, 1);
lean_inc(x_4);
lean_dec(x_1);
x_5 = lean_ctor_get(x_3, 0);
lean_inc(x_5);
x_6 = lean_ctor_get(x_3, 1);
lean_inc(x_6);
lean_dec(x_3);
x_7 = l_Nat_Linear_monomialToExpr(x_5, x_6);
x_8 = l_Nat_Linear_Poly_toExpr_go(x_7, x_4);
return x_8;
}
}
}
LEAN_EXPORT lean_object* l_Nat_Linear_PolyCnstr_toExpr(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = lean_ctor_get_uint8(x_1, sizeof(void*)*2);
x_3 = lean_ctor_get(x_1, 0);
lean_inc(x_3);
x_4 = lean_ctor_get(x_1, 1);
lean_inc(x_4);
lean_dec(x_1);
x_5 = l_Nat_Linear_Poly_toExpr(x_3);
x_6 = l_Nat_Linear_Poly_toExpr(x_4);
x_7 = lean_alloc_ctor(0, 2, 1);
lean_ctor_set(x_7, 0, x_5);
lean_ctor_set(x_7, 1, x_6);
lean_ctor_set_uint8(x_7, sizeof(void*)*2, x_2);
return x_7;
}
}
lean_object* initialize_Init_Coe(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Classical(uint8_t builtin, lean_object*);
lean_object* initialize_Init_SimpLemmas(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_Nat_Basic(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_List_Basic(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_Prod(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Init_Data_Nat_Linear(uint8_t builtin, lean_object* w) {
lean_object * res;
@ -2639,6 +3007,9 @@ lean_dec_ref(res);
res = initialize_Init_Data_List_Basic(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Prod(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Nat_Linear_fixedVar = _init_l_Nat_Linear_fixedVar();
lean_mark_persistent(l_Nat_Linear_fixedVar);
l_Nat_Linear_instInhabitedExpr___closed__1 = _init_l_Nat_Linear_instInhabitedExpr___closed__1();
@ -2649,6 +3020,10 @@ l_Nat_Linear_Poly_isNum_x3f___closed__1 = _init_l_Nat_Linear_Poly_isNum_x3f___cl
lean_mark_persistent(l_Nat_Linear_Poly_isNum_x3f___closed__1);
l_Nat_Linear_Expr_inc___closed__1 = _init_l_Nat_Linear_Expr_inc___closed__1();
lean_mark_persistent(l_Nat_Linear_Expr_inc___closed__1);
l_Nat_Linear_instBEqPolyCnstr___closed__1 = _init_l_Nat_Linear_instBEqPolyCnstr___closed__1();
lean_mark_persistent(l_Nat_Linear_instBEqPolyCnstr___closed__1);
l_Nat_Linear_instBEqPolyCnstr = _init_l_Nat_Linear_instBEqPolyCnstr();
lean_mark_persistent(l_Nat_Linear_instBEqPolyCnstr);
l_Nat_Linear_Certificate_combine___closed__1 = _init_l_Nat_Linear_Certificate_combine___closed__1();
lean_mark_persistent(l_Nat_Linear_Certificate_combine___closed__1);
return lean_io_result_mk_ok(lean_box(0));

29
stage0/stdlib/Init/Data/Prod.c generated Normal file
View file

@ -0,0 +1,29 @@
// Lean compiler output
// Module: Init.Data.Prod
// Imports: Init.SimpLemmas
#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* initialize_Init_SimpLemmas(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Init_Data_Prod(uint8_t builtin, lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init_SimpLemmas(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus
}
#endif

1785
stage0/stdlib/Init/Meta.c generated
View file

File diff suppressed because it is too large Load diff

3
stage0/stdlib/Lean/Elab/PreDefinition/Structural/Eqns.c generated
View file

@ -361,7 +361,7 @@ x_1 = l_Lean_Meta_Simp_defaultMaxSteps;
x_2 = lean_unsigned_to_nat(2u);
x_3 = 0;
x_4 = 1;
x_5 = lean_alloc_ctor(0, 2, 10);
x_5 = lean_alloc_ctor(0, 2, 11);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
lean_ctor_set_uint8(x_5, sizeof(void*)*2, x_3);
@ -374,6 +374,7 @@ lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 6, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 7, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 8, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 9, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 10, x_4);
return x_5;
}
}

3
stage0/stdlib/Lean/Elab/PreDefinition/WF/Eqns.c generated
View file

@ -2002,7 +2002,7 @@ x_1 = l_Lean_Meta_Simp_defaultMaxSteps;
x_2 = lean_unsigned_to_nat(2u);
x_3 = 0;
x_4 = 1;
x_5 = lean_alloc_ctor(0, 2, 10);
x_5 = lean_alloc_ctor(0, 2, 11);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
lean_ctor_set_uint8(x_5, sizeof(void*)*2, x_3);
@ -2015,6 +2015,7 @@ lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 6, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 7, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 8, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 9, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 10, x_4);
return x_5;
}
}

6
stage0/stdlib/Lean/Elab/Tactic/Simp.c generated
View file

@ -803,7 +803,7 @@ x_1 = l_Lean_Meta_Simp_defaultMaxSteps;
x_2 = lean_unsigned_to_nat(2u);
x_3 = 0;
x_4 = 1;
x_5 = lean_alloc_ctor(0, 2, 10);
x_5 = lean_alloc_ctor(0, 2, 11);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
lean_ctor_set_uint8(x_5, sizeof(void*)*2, x_3);
@ -816,6 +816,7 @@ lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 6, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 7, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 8, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 9, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 10, x_4);
return x_5;
}
}
@ -1171,7 +1172,7 @@ x_1 = l_Lean_Meta_Simp_defaultMaxSteps;
x_2 = lean_unsigned_to_nat(2u);
x_3 = 1;
x_4 = 0;
x_5 = lean_alloc_ctor(0, 2, 10);
x_5 = lean_alloc_ctor(0, 2, 11);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
lean_ctor_set_uint8(x_5, sizeof(void*)*2, x_3);
@ -1184,6 +1185,7 @@ lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 6, x_3);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 7, x_3);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 8, x_3);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 9, x_3);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 10, x_3);
return x_5;
}
}

6
stage0/stdlib/Lean/Meta/Tactic/LinearArith.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Meta.Tactic.LinearArith
// Imports: Init Lean.Meta.Tactic.LinearArith.Basic
// Imports: Init Lean.Meta.Tactic.LinearArith.Basic Lean.Meta.Tactic.LinearArith.Nat
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -15,6 +15,7 @@ extern "C" {
#endif
lean_object* initialize_Init(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Meta_Tactic_LinearArith_Basic(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Meta_Tactic_LinearArith_Nat(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Lean_Meta_Tactic_LinearArith(uint8_t builtin, lean_object* w) {
lean_object * res;
@ -26,6 +27,9 @@ lean_dec_ref(res);
res = initialize_Lean_Meta_Tactic_LinearArith_Basic(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Meta_Tactic_LinearArith_Nat(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

4223
stage0/stdlib/Lean/Meta/Tactic/LinearArith/Nat.c generated
View file

File diff suppressed because it is too large Load diff

6
stage0/stdlib/Lean/Meta/Tactic/Simp/Types.c generated
View file

@ -166,7 +166,7 @@ x_1 = l_Lean_Meta_Simp_defaultMaxSteps;
x_2 = lean_unsigned_to_nat(2u);
x_3 = 0;
x_4 = 1;
x_5 = lean_alloc_ctor(0, 2, 10);
x_5 = lean_alloc_ctor(0, 2, 11);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
lean_ctor_set_uint8(x_5, sizeof(void*)*2, x_3);
@ -179,6 +179,7 @@ lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 6, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 7, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 8, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 9, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 10, x_4);
return x_5;
}
}
@ -306,7 +307,7 @@ _start:
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(0u);
x_2 = 0;
x_3 = lean_alloc_ctor(0, 2, 10);
x_3 = lean_alloc_ctor(0, 2, 11);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_1);
lean_ctor_set_uint8(x_3, sizeof(void*)*2, x_2);
@ -319,6 +320,7 @@ lean_ctor_set_uint8(x_3, sizeof(void*)*2 + 6, x_2);
lean_ctor_set_uint8(x_3, sizeof(void*)*2 + 7, x_2);
lean_ctor_set_uint8(x_3, sizeof(void*)*2 + 8, x_2);
lean_ctor_set_uint8(x_3, sizeof(void*)*2 + 9, x_2);
lean_ctor_set_uint8(x_3, sizeof(void*)*2 + 10, x_2);
return x_3;
}
}