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 2021-02-16 10:47:15 -08:00
parent 504a015f9b
commit 186c620f59
39 changed files with 8464 additions and 3503 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
stage0/src/Init.lean generated
View file

@ -17,3 +17,4 @@ import Init.Fix
import Init.Meta
import Init.NotationExtra
import Init.SimpLemmas
import Init.Hints

12
stage0/src/Init/Hints.lean generated Normal file
View file

@ -0,0 +1,12 @@
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.NotationExtra
/- Hint for making sure `Not p` is definitionally equal to `p → False` even when
`TransparencyMode.reducible` -/
unif_hint (p : Prop) where
|- Not p =?= p → False

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

@ -843,6 +843,7 @@ structure Config where
iota : Bool := true
proj : Bool := true
ctorEq : Bool := true
decide : Bool := true
deriving Inhabited, BEq, Repr
end Meta.Simp

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

@ -488,7 +488,7 @@ instance : Pow Nat where
set_option bootstrap.genMatcherCode false in
@[extern "lean_nat_dec_eq"]
def Nat.beq : Nat → Nat → Bool
def Nat.beq : (@& Nat) → (@& Nat) → Bool
| zero, zero => true
| zero, succ m => false
| succ n, zero => false
@ -521,7 +521,7 @@ protected def Nat.decEq (n m : @& Nat) : Decidable (Eq n m) :=
set_option bootstrap.genMatcherCode false in
@[extern "lean_nat_dec_le"]
def Nat.ble : Nat → Nat → Bool
def Nat.ble : @& Nat → @& Nat → Bool
| zero, zero => true
| zero, succ m => true
| succ n, zero => false
@ -635,7 +635,7 @@ protected theorem Nat.ltOfLeOfNe {n m : Nat} (h₁ : LessEq n m) (h₂ : Not (Eq
set_option bootstrap.genMatcherCode false in
@[extern c inline "lean_nat_sub(#1, lean_box(1))"]
def Nat.pred : Nat → Nat
def Nat.pred : (@& Nat) → Nat
| 0 => 0
| succ a => a
@ -701,7 +701,7 @@ def UInt8.size : Nat := 256
structure UInt8 where
val : Fin UInt8.size
attribute [extern "lean_uint8_of_nat"] UInt8.mk
attribute [extern "lean_uint8_of_nat_mk"] UInt8.mk
attribute [extern "lean_uint8_to_nat"] UInt8.val
@[extern "lean_uint8_of_nat"]
@ -725,7 +725,7 @@ def UInt16.size : Nat := 65536
structure UInt16 where
val : Fin UInt16.size
attribute [extern "lean_uint16_of_nat"] UInt16.mk
attribute [extern "lean_uint16_of_nat_mk"] UInt16.mk
attribute [extern "lean_uint16_to_nat"] UInt16.val
@[extern "lean_uint16_of_nat"]
@ -749,7 +749,7 @@ def UInt32.size : Nat := 4294967296
structure UInt32 where
val : Fin UInt32.size
attribute [extern "lean_uint32_of_nat"] UInt32.mk
attribute [extern "lean_uint32_of_nat_mk"] UInt32.mk
attribute [extern "lean_uint32_to_nat"] UInt32.val
@[extern "lean_uint32_of_nat"]
@ -797,7 +797,7 @@ def UInt64.size : Nat := 18446744073709551616
structure UInt64 where
val : Fin UInt64.size
attribute [extern "lean_uint64_of_nat"] UInt64.mk
attribute [extern "lean_uint64_of_nat_mk"] UInt64.mk
attribute [extern "lean_uint64_to_nat"] UInt64.val
@[extern "lean_uint64_of_nat"]
@ -828,7 +828,7 @@ theorem usizeSzEq : Or (Eq USize.size 4294967296) (Eq USize.size 184467440737095
structure USize where
val : Fin USize.size
attribute [extern "lean_usize_of_nat"] USize.mk
attribute [extern "lean_usize_of_nat_mk"] USize.mk
attribute [extern "lean_usize_to_nat"] USize.val
@[extern "lean_usize_of_nat"]
@ -878,7 +878,7 @@ private theorem validCharIsUInt32 {n : Nat} (h : n.isValidChar) : Less n UInt32.
| Or.inr ⟨_, h⟩ => Nat.ltTrans h (decide! : Less 1114112 UInt32.size)
@[extern "lean_uint32_of_nat"]
private def Char.ofNatAux (n : Nat) (h : n.isValidChar) : Char :=
private def Char.ofNatAux (n : @& Nat) (h : n.isValidChar) : Char :=
{ val := ⟨{ val := n, isLt := validCharIsUInt32 h }⟩, valid := h }
@[noinline, matchPattern]

28
stage0/src/Init/SimpLemmas.lean generated
View file

@ -20,6 +20,15 @@ theorem eqTrue (h : p) : p = True :=
theorem eqFalse (h : ¬ p) : p = False :=
propext <| Iff.intro (fun h' => absurd h' h) (fun h' => False.elim h')
theorem eqFalse' (h : p → False) : p = False :=
propext <| Iff.intro (fun h' => absurd h' h) (fun h' => False.elim h')
theorem eqTrueOfDecide {p : Prop} {s : Decidable p} (h : decide p = true) : p = True :=
propext <| Iff.intro (fun h => trivial) (fun _ => ofDecideEqTrue h)
theorem eqFalseOfDecide {p : Prop} {s : Decidable p} (h : decide p = false) : p = False :=
propext <| Iff.intro (fun h' => absurd h' (ofDecideEqFalse h)) (fun h => False.elim h)
theorem impCongr {p₁ p₂ : Sort u} {q₁ q₂ : Sort v} (h₁ : p₁ = p₂) (h₂ : q₁ = q₂) : (p₁ → q₁) = (p₂ → q₂) :=
h₁ ▸ h₂ ▸ rfl
@ -60,3 +69,22 @@ theorem diteCongr {s : Decidable b} [Decidable c]
cases Decidable.em c with
| inl h => rw [difPos h]; subst b; rw [difPos h]; exact h₂ h
| inr h => rw [difNeg h]; subst b; rw [difNeg h]; exact h₃ h
namespace Lean.Simp
@[simp] theorem Ne_Eq (a b : α) : (a ≠ b) = Not (a = b) := rfl
@[simp] theorem ite_True (a b : α) : (if True then a else b) = a := rfl
@[simp] theorem ite_False (a b : α) : (if False then a else b) = b := rfl
@[simp] theorem And_self (p : Prop) : (p ∧ p) = p := propext <| Iff.intro (fun h => h.1) (fun h => ⟨h, h⟩)
@[simp] theorem And_True (p : Prop) : (p ∧ True) = p := propext <| Iff.intro (fun h => h.1) (fun h => ⟨h, trivial⟩)
@[simp] theorem True_And (p : Prop) : (True ∧ p) = p := propext <| Iff.intro (fun h => h.2) (fun h => ⟨trivial, h⟩)
@[simp] theorem And_False (p : Prop) : (p ∧ False) = False := propext <| Iff.intro (fun h => h.2) (fun h => False.elim h)
@[simp] theorem False_And (p : Prop) : (False ∧ p) = False := propext <| Iff.intro (fun h => h.1) (fun h => False.elim h)
@[simp] theorem Or_self (p : Prop) : (p ∨ p) = p := propext <| Iff.intro (fun | Or.inl h => h | Or.inr h => h) (fun h => Or.inl h)
@[simp] theorem Or_True (p : Prop) : (p ∨ True) = True := propext <| Iff.intro (fun h => trivial) (fun h => Or.inr trivial)
@[simp] theorem True_Or (p : Prop) : (True ∨ p) = True := propext <| Iff.intro (fun h => trivial) (fun h => Or.inl trivial)
@[simp] theorem Or_False (p : Prop) : (p ∨ False) = p := propext <| Iff.intro (fun | Or.inl h => h | Or.inr h => False.elim h) (fun h => Or.inl h)
@[simp] theorem False_Or (p : Prop) : (False ∨ p) = p := propext <| Iff.intro (fun | Or.inr h => h | Or.inl h => False.elim h) (fun h => Or.inr h)
@[simp] theorem Iff_self (p : Prop) : (p ↔ p) = True := propext <| Iff.intro (fun h => trivial) (fun _ => Iff.intro id id)
end Lean.Simp

23
stage0/src/Lean/Elab/Tactic/Simp.lean generated
View file

@ -74,7 +74,7 @@ def elabSimpConfig (optConfig : Syntax) : TermElabM Meta.Simp.Config := do
evalSimpConfig (← instantiateMVars c)
/-- Return `some c`, if `e` is of the form `c.{?u_1, ..., ?u_n} ?m_1 ... ?m_k` -/
private def isGlobalLemma? (e : Expr) : Option Name :=
private def isGlobalDecl? (e : Expr) : Option Name :=
e.withApp fun f args =>
if f.isConst && args.all (·.isMVar) && f.constLevels!.all (·.isMVar) then
some f.constName!
@ -94,17 +94,22 @@ private def elabSimpLemmas (stx : Syntax) (ctx : Simp.Context) : TacticM Simp.Co
let (g, _) ← getMainGoal
withMVarContext g do
let mut lemmas := ctx.simpLemmas
for simpLemma in stx[1].getSepArgs do
let mut toUnfold : NameSet := {}
for arg in stx[1].getSepArgs do
let post :=
if simpLemma[0].isNone then
if arg[0].isNone then
true
else
simpLemma[0][0].getKind == ``Parser.Tactic.simpPost
let lemma ← elabTerm simpLemma[1] none (mayPostpone := false)
match isGlobalLemma? lemma with
| some declName => lemmas ← lemmas.addConst declName post
| none => lemmas ← lemmas.add lemma post
return { ctx with simpLemmas := lemmas }
arg[0][0].getKind == ``Parser.Tactic.simpPost
let arg ← elabTerm arg[1] none (mayPostpone := false)
match isGlobalDecl? arg with
| some declName =>
if (← isProof arg) then
lemmas ← lemmas.addConst declName post
else
toUnfold := toUnfold.insert declName
| none => lemmas ← lemmas.add arg post
return { ctx with simpLemmas := lemmas, toUnfold := toUnfold }
@[builtinTactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => do
let ctx ← elabSimpLemmas stx[1] { config := (← elabSimpConfig stx[2]), simpLemmas := (← getSimpLemmas), congrLemmas := (← getCongrLemmas) }

12
stage0/src/Lean/Meta/AppBuilder.lean generated
View file

@ -436,10 +436,20 @@ def mkOfEqTrue (h : Expr) : MetaM Expr :=
def mkEqTrue (h : Expr) : MetaM Expr :=
mkAppM ``eqTrue #[h]
/-- Return `eqFalse h` -/
/--
Return `eqFalse h`
`h` must have type definitionally equal to `¬ p` in the current
reducibility setting. -/
def mkEqFalse (h : Expr) : MetaM Expr :=
mkAppM ``eqFalse #[h]
/--
Return `eqFalse' h`
`h` must have type definitionally equal to `p → False` in the current
reducibility setting. -/
def mkEqFalse' (h : Expr) : MetaM Expr :=
mkAppM ``eqFalse' #[h]
def mkImpCongr (h₁ h₂ : Expr) : MetaM Expr :=
mkAppM ``impCongr #[h₁, h₂]

68
stage0/src/Lean/Meta/Tactic/Simp/Rewrite.lean generated
View file

@ -52,6 +52,7 @@ where
| SimpLemmaKind.neg => return type.appArg!
| SimpLemmaKind.eq => return type.appFn!.appArg!
| SimpLemmaKind.iff => return type.appFn!.appArg!
| SimpLemmaKind.ne => mkEq type.appFn!.appArg! type.appArg!
getRHS (kind : SimpLemmaKind) (type : Expr) : MetaM Expr :=
match kind with
@ -59,6 +60,7 @@ where
| SimpLemmaKind.neg => return mkConst `False
| SimpLemmaKind.eq => return type.appArg!
| SimpLemmaKind.iff => return type.appArg!
| SimpLemmaKind.ne => return mkConst `False
finalizeProof (kind : SimpLemmaKind) (proof : Expr) : MetaM Expr :=
match kind with
@ -66,6 +68,7 @@ where
| SimpLemmaKind.iff => mkPropExt proof
| SimpLemmaKind.pos => mkEqTrue proof
| SimpLemmaKind.neg => mkEqFalse proof
| SimpLemmaKind.ne => mkEqFalse proof
tryLemma? (lemma : SimpLemma) : SimpM (Option Result) :=
withNewMCtxDepth do
@ -91,12 +94,73 @@ where
trace[Meta.Tactic.simp.unify]! "{lemma}, failed to unify {lhs} with {e}"
return none
def preDefault (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step := do
def rewriteCtorEq? (e : Expr) : MetaM (Option Result) := withReducibleAndInstances do
match e.eq? with
| none => return none
| some (_, lhs, rhs) =>
let lhs ← whnf lhs
let rhs ← whnf rhs
let env ← getEnv
match lhs.constructorApp? env, rhs.constructorApp? env with
| some (c₁, _), some (c₂, _) =>
if c₁.name != c₂.name then
withLocalDeclD `h e fun h =>
return some { expr := mkConst ``False, proof? := (← mkEqFalse' (← mkLambdaFVars #[h] (← mkNoConfusion (mkConst ``False) h))) }
else
return none
| _, _ => return none
@[inline] def tryRewriteCtorEq (e : Expr) (x : SimpM Step) : SimpM Step := do
match (← rewriteCtorEq? e) with
| some r => return Step.done r
| none => x
def rewriteUsingDecide? (e : Expr) : MetaM (Option Result) := withReducibleAndInstances do
if e.hasFVar || e.hasMVar then
return none
else
try
let d ← mkDecide e
let r ← withDefault <| whnf d
if r.isConstOf ``true then
return some { expr := mkConst ``True, proof? := mkAppN (mkConst ``eqTrueOfDecide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] }
else if r.isConstOf ``false then
let h ← mkEqRefl d
return some { expr := mkConst ``False, proof? := mkAppN (mkConst ``eqFalseOfDecide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] }
else
return none
catch _ =>
return none
@[inline] def tryRewriteUsingDecide (e : Expr) (x : SimpM Step) : SimpM Step := do
if (← read).config.decide then
match (← rewriteUsingDecide? e) with
| some r => return Step.done r
| none => x
else
x
@[inline] def tryUnfold (e : Expr) (x : SimpM Step) : SimpM Step := do
if e.isApp && e.getAppFn.isConst && (← read).toUnfold.contains e.getAppFn.constName! then
-- TODO: try simp lemmas
match (← withDefault <| unfoldDefinition? e) with
| some eNew => return Step.visit { expr := eNew }
| none => x
else
x
def rewritePre (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step := do
let lemmas ← (← read).simpLemmas
return Step.visit (← rewrite e lemmas.pre discharge? (tag := "pre"))
def postDefault (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step := do
def rewritePost (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step := do
let lemmas ← (← read).simpLemmas
return Step.visit (← rewrite e lemmas.post discharge? (tag := "post"))
def preDefault (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step :=
tryRewriteCtorEq e <| rewritePre e discharge?
def postDefault (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step := do
tryRewriteCtorEq e <| tryRewriteUsingDecide e <| tryUnfold e <| rewritePost e discharge?
end Lean.Meta.Simp

6
stage0/src/Lean/Meta/Tactic/Simp/SimpLemmas.lean generated
View file

@ -7,11 +7,12 @@ import Lean.ScopedEnvExtension
import Lean.Util.Recognizers
import Lean.Meta.LevelDefEq
import Lean.Meta.DiscrTree
import Lean.Meta.AppBuilder
namespace Lean.Meta
inductive SimpLemmaKind where
| eq | iff | pos | neg
| eq | iff | ne | pos | neg
deriving Inhabited, BEq
structure SimpLemma where
@ -85,6 +86,9 @@ def mkSimpLemmaCore (e : Expr) (val : Expr) (post : Bool) (prio : Nat) (name? :
match type.iff? with
| some (lhs, rhs) => pure (← DiscrTree.mkPath lhs, ← isPerm lhs rhs, SimpLemmaKind.iff)
| none =>
match type.ne? with
| some (_, lhs, rhs) => pure (← DiscrTree.mkPath (← mkEq lhs rhs), false, SimpLemmaKind.ne)
| none =>
match type.not? with
| some lhs => pure (← DiscrTree.mkPath lhs, false, SimpLemmaKind.neg)
| none => pure (← DiscrTree.mkPath type, false, SimpLemmaKind.pos)

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

@ -21,6 +21,7 @@ structure Context where
config : Config
simpLemmas : SimpLemmas
congrLemmas : CongrLemmas
toUnfold : NameSet := {}
parent? : Option Expr := none
structure State where

6
stage0/src/Lean/PrettyPrinter/Delaborator/Builtins.lean generated
View file

@ -576,7 +576,7 @@ partial def delabDoElems : DelabM (List Syntax) := do
prependAndRec `(doElem|let $n:term ← $ma)
else
prependAndRec `(doElem|$ma:term)
| _ => delabAndRet
| _ => failure
else if e.isLet then
let Expr.letE n t v b _ ← getExpr | unreachable!
let n ← getUnusedName n b
@ -587,10 +587,10 @@ partial def delabDoElems : DelabM (List Syntax) := do
descend b 2 $
prependAndRec `(doElem|let $(mkIdent n) : $stxT := $stxV)
else
delabAndRet
let stx ← delab
[←`(doElem|$stx:term)]
where
prependAndRec x : DelabM _ := List.cons <$> x <*> delabDoElems
delabAndRet : DelabM _ := do let stx ← delab; [←`(doElem|$stx:term)]
@[builtinDelab app.Bind.bind]
def delabDo : Delab := whenPPOption getPPNotation do

3
stage0/src/Lean/Util/Recognizers.lean generated
View file

@ -40,6 +40,9 @@ namespace Expr
@[inline] def eq? (p : Expr) : Option (Expr × Expr × Expr) :=
p.app3? ``Eq
@[inline] def ne? (p : Expr) : Option (Expr × Expr × Expr) :=
p.app3? ``Ne
@[inline] def iff? (p : Expr) : Option (Expr × Expr) :=
p.app2? ``Iff

10
stage0/src/include/lean/lean.h generated
View file

@ -1648,6 +1648,8 @@ static inline uint8_t lean_int_dec_nonneg(b_lean_obj_arg a) {
uint8_t lean_uint8_of_big_nat(b_lean_obj_arg a);
static inline uint8_t lean_uint8_of_nat(b_lean_obj_arg a) { return lean_is_scalar(a) ? (uint8_t)(lean_unbox(a)) : lean_uint8_of_big_nat(a); }
/* Remark: the following function is used to implement the constructor `UInt8.mk`. We can't annotate constructors with `@&` */
static inline uint8_t lean_uint8_of_nat_mk(lean_obj_arg a) { uint8_t r = lean_uint8_of_nat(a); lean_dec(a); return r; }
static inline lean_obj_res lean_uint8_to_nat(uint8_t a) { return lean_usize_to_nat((size_t)a); }
static inline uint8_t lean_uint8_add(uint8_t a1, uint8_t a2) { return a1+a2; }
static inline uint8_t lean_uint8_sub(uint8_t a1, uint8_t a2) { return a1-a2; }
@ -1670,6 +1672,8 @@ static inline uint8_t lean_uint8_dec_le(uint8_t a1, uint8_t a2) { return a1 <= a
uint16_t lean_uint16_of_big_nat(b_lean_obj_arg a);
static inline uint16_t lean_uint16_of_nat(b_lean_obj_arg a) { return lean_is_scalar(a) ? (int16_t)(lean_unbox(a)) : lean_uint16_of_big_nat(a); }
/* Remark: the following function is used to implement the constructor `UInt16.mk`. We can't annotate constructors with `@&` */
static inline uint16_t lean_uint16_of_nat_mk(lean_obj_arg a) { uint16_t r = lean_uint16_of_nat(a); lean_dec(a); return r; }
static inline lean_obj_res lean_uint16_to_nat(uint16_t a) { return lean_usize_to_nat((size_t)a); }
static inline uint16_t lean_uint16_add(uint16_t a1, uint16_t a2) { return a1+a2; }
static inline uint16_t lean_uint16_sub(uint16_t a1, uint16_t a2) { return a1-a2; }
@ -1692,6 +1696,8 @@ static inline uint8_t lean_uint16_dec_le(uint16_t a1, uint16_t a2) { return a1 <
uint32_t lean_uint32_of_big_nat(b_lean_obj_arg a);
static inline uint32_t lean_uint32_of_nat(b_lean_obj_arg a) { return lean_is_scalar(a) ? (uint32_t)(lean_unbox(a)) : lean_uint32_of_big_nat(a); }
/* Remark: the following function is used to implement the constructor `UInt32.mk`. We can't annotate constructors with `@&` */
static inline uint32_t lean_uint32_of_nat_mk(lean_obj_arg a) { uint32_t r = lean_uint32_of_nat(a); lean_dec(a); return r; }
static inline lean_obj_res lean_uint32_to_nat(uint32_t a) { return lean_usize_to_nat((size_t)a); }
static inline uint32_t lean_uint32_add(uint32_t a1, uint32_t a2) { return a1+a2; }
static inline uint32_t lean_uint32_sub(uint32_t a1, uint32_t a2) { return a1-a2; }
@ -1719,6 +1725,8 @@ static inline uint8_t lean_uint32_dec_le(uint32_t a1, uint32_t a2) { return a1 <
uint64_t lean_uint64_of_big_nat(b_lean_obj_arg a);
static inline uint64_t lean_uint64_of_nat(b_lean_obj_arg a) { return lean_is_scalar(a) ? (uint64_t)(lean_unbox(a)) : lean_uint64_of_big_nat(a); }
/* Remark: the following function is used to implement the constructor `UInt64.mk`. We can't annotate constructors with `@&` */
static inline uint64_t lean_uint64_of_nat_mk(lean_obj_arg a) { uint64_t r = lean_uint64_of_nat(a); lean_dec(a); return r; }
static inline uint64_t lean_uint64_add(uint64_t a1, uint64_t a2) { return a1+a2; }
static inline uint64_t lean_uint64_sub(uint64_t a1, uint64_t a2) { return a1-a2; }
static inline uint64_t lean_uint64_mul(uint64_t a1, uint64_t a2) { return a1*a2; }
@ -1741,6 +1749,8 @@ static inline uint8_t lean_uint64_dec_le(uint64_t a1, uint64_t a2) { return a1 <
size_t lean_usize_of_big_nat(b_lean_obj_arg a);
static inline size_t lean_usize_of_nat(b_lean_obj_arg a) { return lean_is_scalar(a) ? lean_unbox(a) : lean_usize_of_big_nat(a); }
/* Remark: the following function is used to implement the constructor `USize.mk`. We can't annotate constructors with `@&` */
static inline size_t lean_usize_of_nat_mk(lean_obj_arg a) { size_t r = lean_usize_of_nat(a); lean_dec(a); return r; }
static inline size_t lean_usize_add(size_t a1, size_t a2) { return a1+a2; }
static inline size_t lean_usize_sub(size_t a1, size_t a2) { return a1-a2; }
static inline size_t lean_usize_mul(size_t a1, size_t a2) { return a1*a2; }

2
stage0/stdlib/CMakeLists.txt generated
View file

File diff suppressed because one or more lines are too long

6
stage0/stdlib/Init.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init
// Imports: Init.Prelude Init.Notation Init.Core Init.Control Init.Data.Basic Init.WF Init.Data Init.System Init.Util Init.Fix Init.Meta Init.NotationExtra Init.SimpLemmas
// Imports: Init.Prelude Init.Notation Init.Core Init.Control Init.Data.Basic Init.WF Init.Data Init.System Init.Util Init.Fix Init.Meta Init.NotationExtra Init.SimpLemmas Init.Hints
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -26,6 +26,7 @@ lean_object* initialize_Init_Fix(lean_object*);
lean_object* initialize_Init_Meta(lean_object*);
lean_object* initialize_Init_NotationExtra(lean_object*);
lean_object* initialize_Init_SimpLemmas(lean_object*);
lean_object* initialize_Init_Hints(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init(lean_object* w) {
lean_object * res;
@ -70,6 +71,9 @@ lean_dec_ref(res);
res = initialize_Init_SimpLemmas(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Hints(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

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

@ -398,6 +398,7 @@ x_9 = lean_unsigned_to_nat(32u);
x_10 = lean_nat_add(x_2, x_9);
lean_dec(x_2);
x_11 = l_Char_ofNat(x_10);
lean_dec(x_10);
return x_11;
}
}
@ -446,6 +447,7 @@ x_9 = lean_unsigned_to_nat(32u);
x_10 = lean_nat_sub(x_2, x_9);
lean_dec(x_2);
x_11 = l_Char_ofNat(x_10);
lean_dec(x_10);
return x_11;
}
}

29
stage0/stdlib/Init/Hints.c generated Normal file
View file

@ -0,0 +1,29 @@
// Lean compiler output
// Module: Init.Hints
// Imports: Init.NotationExtra
#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_NotationExtra(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Hints(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init_NotationExtra(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

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

File diff suppressed because it is too large Load diff

40
stage0/stdlib/Init/Prelude.c generated
View file

@ -42,9 +42,9 @@ lean_object* l_Lean_PrettyPrinter_instMonadQuotationUnexpandM___closed__9;
lean_object* l_USize_mk___boxed(lean_object*);
lean_object* l_withTheReader(lean_object*, lean_object*);
lean_object* l_Nat_sub___boxed(lean_object*, lean_object*);
uint64_t lean_uint64_of_nat(lean_object*);
uint64_t lean_uint64_of_nat_mk(lean_object*);
lean_object* l_Functor_mapConst___default(lean_object*);
size_t lean_usize_of_nat(lean_object*);
size_t lean_usize_of_nat_mk(lean_object*);
lean_object* l_Fin_decLe___boxed(lean_object*);
lean_object* l_Array_getD___rarg(lean_object*, lean_object*, lean_object*);
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
@ -251,7 +251,7 @@ lean_object* l___private_Init_Prelude_0__Lean_extractMainModule(lean_object*, le
lean_object* l_ReaderT_instMonadReaderT(lean_object*, lean_object*);
lean_object* l_System_Platform_getNumBits___boxed(lean_object*);
lean_object* l_EStateM_instMonadStateOfEStateM___closed__3;
uint32_t lean_uint32_of_nat(lean_object*);
uint32_t lean_uint32_of_nat_mk(lean_object*);
uint8_t l_instDecidableEqUInt64(uint64_t, uint64_t);
lean_object* l_EStateM_instMonadEStateM___closed__8;
lean_object* l_Lean_extractMacroScopes_match__1(lean_object*);
@ -396,7 +396,7 @@ lean_object* l_typedExpr___rarg___boxed(lean_object*);
lean_object* l_Lean_Macro_instMonadRefMacroM;
lean_object* l_Lean_Macro_throwError(lean_object*);
lean_object* l_Lean_Macro_instMonadQuotationMacroM___lambda__1(lean_object*, lean_object*);
uint8_t lean_uint8_of_nat(lean_object*);
uint8_t lean_uint8_of_nat_mk(lean_object*);
lean_object* l_Lean_scientificLitKind___closed__2;
lean_object* l_List_set(lean_object*);
lean_object* l_Lean_Syntax_getArg_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -510,7 +510,7 @@ lean_object* l_Monad_seq___default(lean_object*);
lean_object* l_or_match__1___rarg(uint8_t, lean_object*, lean_object*);
lean_object* l_Monad_seqLeft___default___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_instMonadLiftT__1___rarg___boxed(lean_object*);
uint16_t lean_uint16_of_nat(lean_object*);
uint16_t lean_uint16_of_nat_mk(lean_object*);
lean_object* l___private_Init_Prelude_0__Lean_assembleParts_match__1(lean_object*);
lean_object* l_Lean_Syntax_setKind_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Prelude_0__Lean_assembleParts(lean_object*, lean_object*);
@ -753,6 +753,7 @@ lean_object* l_instInhabitedArrow___rarg(lean_object*, lean_object*);
lean_object* l_EStateM_instInhabitedEStateM___rarg(lean_object*, lean_object*);
lean_object* l_Function_const(lean_object*, lean_object*);
lean_object* l_instDecidableEqChar_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Char_ofNat___boxed(lean_object*);
lean_object* l_ReaderT_map(lean_object*, lean_object*);
lean_object* l_System_Platform_numBits___closed__1;
lean_object* l_instDecidableLess___boxed(lean_object*, lean_object*);
@ -2389,6 +2390,8 @@ _start:
{
uint8_t x_3; lean_object* x_4;
x_3 = lean_nat_dec_eq(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
}
@ -2475,6 +2478,8 @@ _start:
{
uint8_t x_3; lean_object* x_4;
x_3 = lean_nat_dec_le(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
}
@ -2522,6 +2527,7 @@ _start:
{
lean_object* x_2;
x_2 = lean_nat_sub(x_1, lean_box(1));
lean_dec(x_1);
return x_2;
}
}
@ -2778,7 +2784,7 @@ lean_object* l_UInt8_mk___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = lean_uint8_of_nat(x_1);
x_2 = lean_uint8_of_nat_mk(x_1);
x_3 = lean_box(x_2);
return x_3;
}
@ -2866,7 +2872,7 @@ lean_object* l_UInt16_mk___boxed(lean_object* x_1) {
_start:
{
uint16_t x_2; lean_object* x_3;
x_2 = lean_uint16_of_nat(x_1);
x_2 = lean_uint16_of_nat_mk(x_1);
x_3 = lean_box(x_2);
return x_3;
}
@ -2954,7 +2960,7 @@ lean_object* l_UInt32_mk___boxed(lean_object* x_1) {
_start:
{
uint32_t x_2; lean_object* x_3;
x_2 = lean_uint32_of_nat(x_1);
x_2 = lean_uint32_of_nat_mk(x_1);
x_3 = lean_box_uint32(x_2);
return x_3;
}
@ -3144,7 +3150,7 @@ lean_object* l_UInt64_mk___boxed(lean_object* x_1) {
_start:
{
uint64_t x_2; lean_object* x_3;
x_2 = lean_uint64_of_nat(x_1);
x_2 = lean_uint64_of_nat_mk(x_1);
x_3 = lean_box_uint64(x_2);
return x_3;
}
@ -3242,7 +3248,7 @@ lean_object* l_USize_mk___boxed(lean_object* x_1) {
_start:
{
size_t x_2; lean_object* x_3;
x_2 = lean_usize_of_nat(x_1);
x_2 = lean_usize_of_nat_mk(x_1);
x_3 = lean_box_usize(x_2);
return x_3;
}
@ -3333,6 +3339,7 @@ _start:
{
uint32_t x_3; lean_object* x_4;
x_3 = lean_uint32_of_nat(x_1);
lean_dec(x_1);
x_4 = lean_box_uint32(x_3);
return x_4;
}
@ -3342,7 +3349,7 @@ _start:
{
lean_object* x_1; uint32_t x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_uint32_of_nat(x_1);
x_2 = lean_uint32_of_nat_mk(x_1);
x_3 = lean_box_uint32(x_2);
return x_3;
}
@ -3361,7 +3368,6 @@ x_5 = lean_nat_dec_lt(x_4, x_1);
if (x_5 == 0)
{
lean_object* x_6;
lean_dec(x_1);
x_6 = l_Char_ofNat___closed__1;
return x_6;
}
@ -3373,7 +3379,6 @@ x_8 = lean_nat_dec_lt(x_1, x_7);
if (x_8 == 0)
{
lean_object* x_9;
lean_dec(x_1);
x_9 = l_Char_ofNat___closed__1;
return x_9;
}
@ -3395,6 +3400,15 @@ return x_13;
}
}
}
lean_object* l_Char_ofNat___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Char_ofNat(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* l_instDecidableEqChar_match__1___rarg(uint8_t x_1, lean_object* x_2, lean_object* x_3) {
_start:
{

14
stage0/stdlib/Lean/Compiler/IR/Format.c generated
View file

@ -33,7 +33,6 @@ lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatExpr___closed_
lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatExpr___closed__3;
extern lean_object* l_termDepIfThenElse___closed__11;
lean_object* l_Lean_IR_formatFnBodyHead___closed__33;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__4;
lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatExpr___closed__15;
extern lean_object* l_Lean_IR_instToStringJoinPointId___closed__1;
lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatIRType___closed__9;
@ -50,6 +49,7 @@ lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatIRType___close
lean_object* l_Lean_IR_formatFnBodyHead___closed__24;
extern lean_object* l_Std_Format_join___closed__1;
lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatExpr___closed__22;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__4;
lean_object* l_Lean_IR_instToStringIRType___closed__1;
lean_object* l_Lean_IR_formatFnBody_loop(lean_object*, lean_object*);
extern lean_object* l_Lean_instInhabitedParserDescr___closed__1;
@ -3432,7 +3432,7 @@ x_13 = l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatIRType(x_3);
x_14 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_14, 0, x_12);
lean_ctor_set(x_14, 1, x_13);
x_15 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__4;
x_15 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__4;
x_16 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_16, 0, x_14);
lean_ctor_set(x_16, 1, x_15);
@ -3525,7 +3525,7 @@ x_53 = l_Lean_IR_formatFnBodyHead___closed__9;
x_54 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_54, 0, x_53);
lean_ctor_set(x_54, 1, x_52);
x_55 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__4;
x_55 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__4;
x_56 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_56, 0, x_54);
lean_ctor_set(x_56, 1, x_55);
@ -3633,7 +3633,7 @@ x_103 = l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatIRType(x_84);
x_104 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_104, 0, x_102);
lean_ctor_set(x_104, 1, x_103);
x_105 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__4;
x_105 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__4;
x_106 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_106, 0, x_104);
lean_ctor_set(x_106, 1, x_105);
@ -4356,7 +4356,7 @@ x_15 = l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatIRType(x_4);
x_16 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_16, 0, x_14);
lean_ctor_set(x_16, 1, x_15);
x_17 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__4;
x_17 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__4;
x_18 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_18, 0, x_16);
lean_ctor_set(x_18, 1, x_17);
@ -4506,7 +4506,7 @@ x_82 = l_Lean_IR_formatFnBodyHead___closed__9;
x_83 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_83, 0, x_82);
lean_ctor_set(x_83, 1, x_81);
x_84 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__4;
x_84 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__4;
x_85 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_85, 0, x_83);
lean_ctor_set(x_85, 1, x_84);
@ -4642,7 +4642,7 @@ x_146 = l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatIRType(x_126);
x_147 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_147, 0, x_145);
lean_ctor_set(x_147, 1, x_146);
x_148 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__4;
x_148 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__4;
x_149 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_149, 0, x_147);
lean_ctor_set(x_149, 1, x_148);

8
stage0/stdlib/Lean/Data/Format.c generated
View file

@ -20,10 +20,10 @@ lean_object* l_Std_Format_format_unicode___closed__1;
lean_object* l_Lean_Option_register___at_Std_Format_initFn____x40_Lean_Data_Format___hyg_25____spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_Format_pretty_x27(lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__4;
lean_object* l_Std_Format_joinSep___at_Lean_formatKVMap___spec__1(lean_object*, lean_object*);
extern lean_object* l_Std_Format_defWidth;
lean_object* l_Std_Format_initFn____x40_Lean_Data_Format___hyg_25____closed__2;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__4;
lean_object* l_Std_Format_getWidth(lean_object*);
extern lean_object* l_Lean_instInhabitedParserDescr___closed__1;
extern lean_object* l_instReprSigma___rarg___closed__1;
@ -865,7 +865,7 @@ x_4 = l_Lean_Name_toString___closed__1;
x_5 = l_Lean_Name_toStringWithSep(x_4, x_2);
x_6 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_6, 0, x_5);
x_7 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__4;
x_7 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__4;
x_8 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_8, 0, x_6);
lean_ctor_set(x_8, 1, x_7);
@ -1018,7 +1018,7 @@ x_8 = l_Lean_Name_toString___closed__1;
x_9 = l_Lean_Name_toStringWithSep(x_8, x_6);
x_10 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_10, 0, x_9);
x_11 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__4;
x_11 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__4;
x_12 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_12, 0, x_10);
lean_ctor_set(x_12, 1, x_11);
@ -1156,7 +1156,7 @@ x_52 = l_Lean_Name_toString___closed__1;
x_53 = l_Lean_Name_toStringWithSep(x_52, x_50);
x_54 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_54, 0, x_53);
x_55 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__4;
x_55 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__4;
x_56 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_56, 0, x_54);
lean_ctor_set(x_56, 1, x_55);

2
stage0/stdlib/Lean/Data/Json/Parser.c generated
View file

@ -1618,6 +1618,7 @@ x_47 = lean_nat_add(x_46, x_38);
lean_dec(x_38);
lean_dec(x_46);
x_48 = l_Char_ofNat(x_47);
lean_dec(x_47);
x_49 = lean_unbox_uint32(x_48);
lean_dec(x_48);
x_50 = lean_box_uint32(x_49);
@ -1651,6 +1652,7 @@ x_61 = lean_nat_add(x_60, x_52);
lean_dec(x_52);
lean_dec(x_60);
x_62 = l_Char_ofNat(x_61);
lean_dec(x_61);
x_63 = lean_unbox_uint32(x_62);
lean_dec(x_62);
x_64 = lean_box_uint32(x_63);

18
stage0/stdlib/Lean/Data/Position.c generated
View file

@ -19,16 +19,16 @@ lean_object* lean_nat_div(lean_object*, lean_object*);
uint8_t l___private_Lean_Data_Position_0__Lean_decEqPosition____x40_Lean_Data_Position___hyg_16_(lean_object*, lean_object*);
extern lean_object* l_instReprSigma___rarg___closed__2;
lean_object* l_Lean_FileMap_ofString_loop(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__4;
lean_object* l_Lean_FileMap_ofString___closed__2;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__27;
lean_object* l_Lean_instInhabitedPosition;
extern lean_object* l_Array_empty___closed__1;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__4;
extern lean_object* l_Lean_instInhabitedParserDescr___closed__1;
extern lean_object* l_instReprSigma___rarg___closed__1;
lean_object* l_Nat_decLt___boxed(lean_object*, lean_object*);
extern lean_object* l_instInhabitedNat;
extern lean_object* l_instReprSigma___rarg___closed__7;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__27;
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
lean_object* lean_string_append(lean_object*, lean_object*);
@ -45,7 +45,6 @@ lean_object* l___private_Lean_Data_Position_0__Lean_reprPosition____x40_Lean_Dat
lean_object* l_Lean_FileMap_toPosition_toColumn(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Position_0__Lean_decEqPosition____x40_Lean_Data_Position___hyg_16__match__1___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__25;
lean_object* l_Lean_Position_instToStringPosition_match__1(lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l_Array_back___at_Lean_FileMap_toPosition___spec__1___boxed(lean_object*);
@ -54,6 +53,7 @@ lean_object* l_Lean_instReprPosition___closed__1;
lean_object* l_Lean_FileMap_toPosition_match__1___rarg(lean_object*, lean_object*);
lean_object* l_Nat_repr(lean_object*);
extern lean_object* l_instReprSigma___rarg___closed__5;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__28;
lean_object* l_Lean_Position_instToFormatPosition_match__1___rarg(lean_object*, lean_object*);
uint32_t lean_string_utf8_get(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Position_0__Lean_reprPosition____x40_Lean_Data_Position___hyg_115____closed__1;
@ -79,8 +79,8 @@ lean_object* l_Lean_Position_lt___closed__1;
lean_object* l_Lean_Position_instToFormatPosition_match__1(lean_object*);
lean_object* l_Lean_instInhabitedPosition___closed__1;
extern lean_object* l_Lean_mkOptionalNode___closed__2;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__26;
lean_object* l___private_Lean_Data_Position_0__Lean_reprPosition____x40_Lean_Data_Position___hyg_115_(lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__26;
lean_object* l___private_Lean_Data_Position_0__Lean_reprPosition____x40_Lean_Data_Position___hyg_115____closed__4;
extern lean_object* l_instReprSigma___rarg___closed__6;
uint8_t lean_string_utf8_at_end(lean_object*, lean_object*);
@ -227,7 +227,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Data_Position_0__Lean_reprPosition____x40_Lean_Data_Position___hyg_115____closed__3;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__4;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__4;
x_3 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -277,7 +277,7 @@ x_12 = l___private_Lean_Data_Position_0__Lean_reprPosition____x40_Lean_Data_Posi
x_13 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_13, 0, x_11);
lean_ctor_set(x_13, 1, x_12);
x_14 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__4;
x_14 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__4;
x_15 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_15, 0, x_13);
lean_ctor_set(x_15, 1, x_14);
@ -290,15 +290,15 @@ lean_ctor_set(x_18, 0, x_17);
x_19 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_19, 0, x_15);
lean_ctor_set(x_19, 1, x_18);
x_20 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__26;
x_20 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__27;
x_21 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_19);
x_22 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__27;
x_22 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__28;
x_23 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_23, 0, x_21);
lean_ctor_set(x_23, 1, x_22);
x_24 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__25;
x_24 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__26;
x_25 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_25, 0, x_24);
lean_ctor_set(x_25, 1, x_23);

28
stage0/stdlib/Lean/DeclarationRange.c generated
View file

@ -25,16 +25,15 @@ uint8_t l___private_Lean_Data_Position_0__Lean_decEqPosition____x40_Lean_Data_Po
lean_object* l_Lean_PersistentEnvExtension_getModuleEntries___rarg(lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_findDeclarationRanges_x3f___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__4;
extern lean_object* l_Lean_noConfusionExt;
lean_object* l_Lean_declRangeExt___elambda__2(lean_object*);
uint8_t l_Lean_Name_quickLt(lean_object*, lean_object*);
lean_object* l_Array_binSearch___at_Lean_findDeclarationRangesCore_x3f___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerInternalExceptionId___closed__2;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__27;
lean_object* l_Lean_addDeclarationRanges(lean_object*);
lean_object* l_Lean_instReprDeclarationRanges___closed__1;
extern lean_object* l_Array_empty___closed__1;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__4;
uint8_t l_Array_anyMUnsafe___at_Array_any___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRange____x40_Lean_DeclarationRange___hyg_203____closed__6;
lean_object* lean_st_ref_get(lean_object*, lean_object*);
@ -42,6 +41,7 @@ lean_object* l___private_Lean_DeclarationRange_0__Lean_decEqDeclarationRange____
lean_object* l_Lean_declRangeExt___elambda__3___boxed(lean_object*, lean_object*);
lean_object* l_Lean_declRangeExt;
lean_object* l_Lean_mkMapDeclarationExtension___at_Lean_initFn____x40_Lean_DeclarationRange___hyg_338____spec__1___lambda__1(lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__27;
lean_object* lean_array_get_size(lean_object*);
lean_object* lean_string_append(lean_object*, lean_object*);
lean_object* l_Lean_instReprDeclarationRange;
@ -64,7 +64,6 @@ lean_object* l_Lean_MapDeclarationExtension_insert___rarg(lean_object*, lean_obj
lean_object* l_Lean_mkMapDeclarationExtension___at_Lean_initFn____x40_Lean_DeclarationRange___hyg_338____spec__1(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_declRangeExt___elambda__4___boxed(lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__25;
lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRanges____x40_Lean_DeclarationRange___hyg_294_(lean_object*, lean_object*);
lean_object* lean_array_swap(lean_object*, lean_object*, lean_object*);
@ -83,6 +82,7 @@ lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___lambda__2(lean
lean_object* l_Array_qsort___at_Lean_initFn____x40_Lean_DeclarationRange___hyg_338____spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_qsort___at_Lean_initFn____x40_Lean_DeclarationRange___hyg_338____spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRange____x40_Lean_DeclarationRange___hyg_203____closed__3;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__28;
lean_object* l_Lean_instInhabitedDeclarationRanges___closed__1;
lean_object* l_Lean_findDeclarationRangesCore_x3f___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRange____x40_Lean_DeclarationRange___hyg_203____closed__10;
@ -140,8 +140,8 @@ lean_object* l_Lean_registerSimplePersistentEnvExtension___at_Lean_initFn____x40
extern lean_object* l_Lean_instInhabitedPosition___closed__1;
lean_object* l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRange____x40_Lean_DeclarationRange___hyg_203____closed__9;
lean_object* l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRange____x40_Lean_DeclarationRange___hyg_203_(lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__26;
lean_object* l___private_Lean_Data_Position_0__Lean_reprPosition____x40_Lean_Data_Position___hyg_115_(lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__26;
lean_object* l_Lean_declRangeExt___elambda__2___boxed(lean_object*);
lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_initFn____x40_Lean_DeclarationRange___hyg_338____spec__6(lean_object*, lean_object*);
lean_object* l_EStateM_pure___rarg(lean_object*, lean_object*);
@ -323,7 +323,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRange____x40_Lean_DeclarationRange___hyg_203____closed__3;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__4;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__4;
x_3 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -408,7 +408,7 @@ x_12 = l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRange____x40_Lea
x_13 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_13, 0, x_11);
lean_ctor_set(x_13, 1, x_12);
x_14 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__4;
x_14 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__4;
x_15 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_15, 0, x_13);
lean_ctor_set(x_15, 1, x_14);
@ -461,15 +461,15 @@ lean_ctor_set(x_35, 0, x_34);
x_36 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_36, 0, x_32);
lean_ctor_set(x_36, 1, x_35);
x_37 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__26;
x_37 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__27;
x_38 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_38, 0, x_37);
lean_ctor_set(x_38, 1, x_36);
x_39 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__27;
x_39 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__28;
x_40 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_40, 0, x_38);
lean_ctor_set(x_40, 1, x_39);
x_41 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__25;
x_41 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__26;
x_42 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_42, 0, x_41);
lean_ctor_set(x_42, 1, x_40);
@ -559,7 +559,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRanges____x40_Lean_DeclarationRange___hyg_294____closed__3;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__4;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__4;
x_3 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -608,7 +608,7 @@ x_12 = l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRanges____x40_Le
x_13 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_13, 0, x_11);
lean_ctor_set(x_13, 1, x_12);
x_14 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__4;
x_14 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__4;
x_15 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_15, 0, x_13);
lean_ctor_set(x_15, 1, x_14);
@ -619,15 +619,15 @@ x_17 = l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRange____x40_Lea
x_18 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_18, 0, x_15);
lean_ctor_set(x_18, 1, x_17);
x_19 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__26;
x_19 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__27;
x_20 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_20, 0, x_19);
lean_ctor_set(x_20, 1, x_18);
x_21 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__27;
x_21 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__28;
x_22 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_22, 0, x_20);
lean_ctor_set(x_22, 1, x_21);
x_23 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__25;
x_23 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__26;
x_24 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_24, 0, x_23);
lean_ctor_set(x_24, 1, x_22);

6
stage0/stdlib/Lean/Elab/InfoTree.c generated
View file

@ -26,7 +26,6 @@ lean_object* l_Lean_Elab_withInfoContext_x27___at_Lean_Elab_withInfoContext___sp
lean_object* l_Array_modify___at_Lean_Elab_assignInfoHoleId___spec__4___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_InternalExceptionId_toString___closed__1;
lean_object* lean_array_uget(lean_object*, size_t);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__4;
lean_object* l_Std_PersistentHashMap_insertAux___at_Lean_Elab_assignInfoHoleId___spec__2___lambda__1(lean_object*, lean_object*, size_t, size_t, size_t, size_t, lean_object*);
lean_object* l_Lean_Elab_pushInfoTree___rarg___lambda__1(lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_find_x3f___at_Lean_Elab_InfoTree_substitute___spec__6(lean_object*, lean_object*);
@ -50,6 +49,7 @@ lean_object* l_Lean_Elab_InfoTree_format_match__1(lean_object*);
extern lean_object* l_Array_empty___closed__1;
lean_object* l_Lean_Meta_ppExpr(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_ContextInfo_runMetaM___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__4;
lean_object* l_Lean_Elab_withInfoContext_x27_match__1(lean_object*);
lean_object* lean_st_ref_get(lean_object*, lean_object*);
lean_object* l_Lean_Elab_enableInfoTree(lean_object*);
@ -2045,7 +2045,7 @@ lean_ctor_set(x_21, 1, x_20);
x_22 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_22, 0, x_21);
lean_ctor_set(x_22, 1, x_11);
x_23 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__4;
x_23 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__4;
x_24 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_24, 0, x_22);
lean_ctor_set(x_24, 1, x_23);
@ -2091,7 +2091,7 @@ lean_ctor_set(x_39, 1, x_38);
x_40 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_40, 0, x_39);
lean_ctor_set(x_40, 1, x_11);
x_41 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__4;
x_41 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__4;
x_42 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_42, 0, x_40);
lean_ctor_set(x_42, 1, x_41);

6
stage0/stdlib/Lean/Elab/Quotation.c generated
View file

@ -587,7 +587,6 @@ extern lean_object* l_instReprList___rarg___closed__2;
lean_object* l_List_map___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___spec__7(lean_object*);
lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___lambda__6___closed__16;
extern lean_object* l_Lean_Parser_Syntax_addPrec___closed__10;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__20;
lean_object* l_Lean_Elab_Term_Quotation_mkTuple___lambda__3___closed__5;
extern lean_object* l_Lean_Parser_Term_quot___elambda__1___closed__1;
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_Quotation_match__syntax_expand___spec__6(size_t, size_t, lean_object*);
@ -791,6 +790,7 @@ lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHead
lean_object* l_List_head_x21___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___spec__1___boxed(lean_object*);
lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___closed__1;
lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__13___closed__5;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__20;
lean_object* l_Array_foldrMUnsafe___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapIdxM_map___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___spec__6___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__23___closed__11;
@ -18282,7 +18282,7 @@ lean_ctor_set(x_39, 0, x_20);
lean_ctor_set(x_39, 1, x_38);
lean_inc(x_2);
x_40 = lean_array_push(x_2, x_39);
x_41 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__20;
x_41 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__20;
lean_inc(x_1);
x_42 = lean_name_mk_string(x_1, x_41);
lean_inc(x_2);
@ -18606,7 +18606,7 @@ lean_ctor_set(x_179, 0, x_20);
lean_ctor_set(x_179, 1, x_178);
lean_inc(x_2);
x_180 = lean_array_push(x_2, x_179);
x_181 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__20;
x_181 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__20;
lean_inc(x_1);
x_182 = lean_name_mk_string(x_1, x_181);
lean_inc(x_2);

4
stage0/stdlib/Lean/Elab/StructInst.c generated
View file

@ -67,7 +67,6 @@ lean_object* l_Lean_Elab_Term_StructInst_instToFormatFieldLHS_match__1___rarg(le
lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_step_match__2(lean_object*);
lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_groupFields___closed__1;
lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_elabStruct_match__6___rarg(lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__4;
lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_findDefaultMissing_x3f_match__2(lean_object*);
lean_object* lean_expr_update_mdata(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_elabModifyOp___closed__6;
@ -117,6 +116,7 @@ lean_object* l_Lean_Elab_Term_StructInst_markDefaultMissing(lean_object*);
extern lean_object* l_Array_empty___closed__1;
lean_object* lean_environment_find(lean_object*, lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_14424____closed__11;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__4;
lean_object* l_Lean_Elab_Term_StructInst_initFn____x40_Lean_Elab_StructInst___hyg_6703_(lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_12336____closed__9;
lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_mkDefaultValueAux_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -5960,7 +5960,7 @@ x_3 = lean_ctor_get(x_2, 1);
lean_inc(x_3);
x_4 = l_Lean_Elab_Term_StructInst_formatField___closed__2;
x_5 = l_Std_Format_joinSep___at_Lean_Elab_Term_StructInst_formatField___spec__1(x_3, x_4);
x_6 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__4;
x_6 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__4;
x_7 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_7, 0, x_5);
lean_ctor_set(x_7, 1, x_6);

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

File diff suppressed because it is too large Load diff

4
stage0/stdlib/Lean/Expr.c generated
View file

@ -467,7 +467,6 @@ lean_object* lean_expr_update_let(lean_object*, lean_object*, lean_object*, lean
uint8_t l_Lean_Expr_isForall(lean_object*);
uint8_t l_Lean_BinderInfo_isInstImplicit(uint8_t);
lean_object* l_Lean_mkDecIsFalse(lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__20;
uint8_t lean_expr_quick_lt(lean_object*, lean_object*);
uint8_t l_Lean_Expr_isLit(lean_object*);
lean_object* l_Lean_mkFVar(lean_object*);
@ -597,6 +596,7 @@ lean_object* l_Lean_Expr_appArg_x21___closed__2;
lean_object* l_Lean_mkApp7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_updateLambda_x21___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_mk_proj(lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__20;
lean_object* l_Lean_Expr_isMVar_match__1(lean_object*);
lean_object* l___private_Lean_Expr_0__Lean_Expr_getAppRevArgsAux_match__1(lean_object*);
lean_object* l_Lean_Expr_appFn_x21___closed__2;
@ -3215,7 +3215,7 @@ return x_12;
default:
{
lean_object* x_13;
x_13 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__20;
x_13 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__20;
return x_13;
}
}

42
stage0/stdlib/Lean/Meta/AppBuilder.c generated
View file

@ -226,6 +226,7 @@ lean_object* l_Lean_Meta_mkAppM___lambda__1___closed__5;
lean_object* l_Lean_Meta_mkForallCongr___closed__2;
lean_object* l_Lean_Meta_mkEqTrans___closed__2;
lean_object* l_Lean_Meta_mkAppM___closed__2;
lean_object* l_Lean_Meta_mkEqFalse_x27___closed__2;
lean_object* l_Lean_Meta_mkProjection_match__3(lean_object*);
lean_object* l_Lean_Meta_mkEqTrue(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkForallCongr___closed__1;
@ -250,6 +251,7 @@ lean_object* l_Lean_Meta_mkEqNDRec___closed__4;
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkAppMFinal___closed__2;
uint8_t l_Lean_Expr_isForall(lean_object*);
lean_object* l_Lean_Meta_mkEqRefl___closed__1;
lean_object* l_Lean_Meta_mkEqFalse_x27___closed__1;
lean_object* l_Lean_Meta_whnf(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkAppMFinal___closed__1;
lean_object* l_Lean_Meta_mkOfEqTrue___closed__1;
@ -325,6 +327,7 @@ lean_object* l_Lean_mkApp4(lean_object*, lean_object*, lean_object*, lean_object
lean_object* l_Lean_Meta_getLevel(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkCongrArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkAppOptMAux_match__1(lean_object*);
lean_object* l_Lean_Meta_mkEqFalse_x27(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_10205____closed__7;
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkAppMFinal___closed__3;
@ -337,7 +340,7 @@ lean_object* l_Lean_Meta_mkEqOfHEq___closed__3;
extern lean_object* l_Lean_Meta_throwLetTypeMismatchMessage___rarg___closed__7;
lean_object* l_Lean_Meta_mkEqMPR___closed__1;
lean_object* l_Lean_Meta_inferType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_AppBuilder___hyg_4144_(lean_object*);
lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_AppBuilder___hyg_4156_(lean_object*);
extern lean_object* l_Lean_instInhabitedMessageData___closed__1;
lean_object* l_Lean_Meta_isExprDefEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_mkFreshExprMVarImpl(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -11914,6 +11917,35 @@ x_10 = l_Lean_Meta_mkAppM(x_9, x_8, x_2, x_3, x_4, x_5, x_6);
return x_10;
}
}
static lean_object* _init_l_Lean_Meta_mkEqFalse_x27___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("eqFalse'");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_mkEqFalse_x27___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_mkEqFalse_x27___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Meta_mkEqFalse_x27(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_7 = l_Lean_mkOptionalNode___closed__2;
x_8 = lean_array_push(x_7, x_1);
x_9 = l_Lean_Meta_mkEqFalse_x27___closed__2;
x_10 = l_Lean_Meta_mkAppM(x_9, x_8, x_2, x_3, x_4, x_5, x_6);
return x_10;
}
}
static lean_object* _init_l_Lean_Meta_mkImpCongr___closed__1() {
_start:
{
@ -12546,7 +12578,7 @@ x_10 = l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkBinaryOp(x_8, x_9, x_1, x
return x_10;
}
}
lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_AppBuilder___hyg_4144_(lean_object* x_1) {
lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_AppBuilder___hyg_4156_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -12802,6 +12834,10 @@ l_Lean_Meta_mkEqFalse___closed__1 = _init_l_Lean_Meta_mkEqFalse___closed__1();
lean_mark_persistent(l_Lean_Meta_mkEqFalse___closed__1);
l_Lean_Meta_mkEqFalse___closed__2 = _init_l_Lean_Meta_mkEqFalse___closed__2();
lean_mark_persistent(l_Lean_Meta_mkEqFalse___closed__2);
l_Lean_Meta_mkEqFalse_x27___closed__1 = _init_l_Lean_Meta_mkEqFalse_x27___closed__1();
lean_mark_persistent(l_Lean_Meta_mkEqFalse_x27___closed__1);
l_Lean_Meta_mkEqFalse_x27___closed__2 = _init_l_Lean_Meta_mkEqFalse_x27___closed__2();
lean_mark_persistent(l_Lean_Meta_mkEqFalse_x27___closed__2);
l_Lean_Meta_mkImpCongr___closed__1 = _init_l_Lean_Meta_mkImpCongr___closed__1();
lean_mark_persistent(l_Lean_Meta_mkImpCongr___closed__1);
l_Lean_Meta_mkImpCongr___closed__2 = _init_l_Lean_Meta_mkImpCongr___closed__2();
@ -12824,7 +12860,7 @@ l_Lean_Meta_mkNumeral___closed__2 = _init_l_Lean_Meta_mkNumeral___closed__2();
lean_mark_persistent(l_Lean_Meta_mkNumeral___closed__2);
l_Lean_Meta_mkNumeral___closed__3 = _init_l_Lean_Meta_mkNumeral___closed__3();
lean_mark_persistent(l_Lean_Meta_mkNumeral___closed__3);
res = l_Lean_Meta_initFn____x40_Lean_Meta_AppBuilder___hyg_4144_(lean_io_mk_world());
res = l_Lean_Meta_initFn____x40_Lean_Meta_AppBuilder___hyg_4156_(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));

38
stage0/stdlib/Lean/Meta/Tactic/Simp/CongrLemmas.c generated
View file

@ -50,7 +50,6 @@ lean_object* l_Std_PersistentHashMap_insertAux___at_Lean_Meta_addCongrLemmaEntry
lean_object* l_Lean_Meta_getCongrLemmas___rarg(lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemma____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_21_(lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkCongrLemma___spec__6(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__4;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkCongrLemma___spec__5___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_LocalContext_fvarIdToDecl___default___closed__1;
lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Meta_mkCongrLemma___spec__10(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -60,7 +59,6 @@ lean_object* l_Lean_Meta_mkCongrLemma_match__4(lean_object*);
lean_object* l_Lean_registerSimpleScopedEnvExtension___rarg(lean_object*, lean_object*);
lean_object* l_Lean_SMap_toList___at___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemmas____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_117____spec__1(lean_object*);
lean_object* l_Lean_Meta_CongrLemmas_get___boxed(lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__27;
lean_object* l___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemmas____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_117____closed__6;
lean_object* l_Lean_SMap_fold___at___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemmas____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_117____spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_CongrLemmas_get(lean_object*, lean_object*);
@ -69,6 +67,7 @@ size_t l_USize_sub(size_t, size_t);
extern lean_object* l_Array_empty___closed__1;
extern lean_object* l_instReprProd___rarg___closed__2;
lean_object* l_Std_HashMapImp_find_x3f___at_Lean_Meta_CongrLemmas_get___spec__5(lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__4;
uint8_t l_Lean_checkTraceOption(lean_object*, lean_object*);
lean_object* lean_st_ref_get(lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_findAtAux___at_Lean_Meta_CongrLemmas_get___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -80,6 +79,7 @@ lean_object* l_Lean_Meta_mkCongrLemma_onlyMVarsAt___boxed(lean_object*, lean_obj
lean_object* l_Std_AssocList_replace___at_Lean_Meta_addCongrLemmaEntry___spec__13(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_appFn_x21(lean_object*);
extern lean_object* l_Lean_instHashableName___closed__1;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__27;
lean_object* l_Array_toSubarray___rarg(lean_object*, lean_object*, lean_object*);
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
@ -136,7 +136,6 @@ lean_object* l___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCong
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
extern lean_object* l_Lean_NameSet_insert___closed__1;
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_forallMetaTelescopeReducingAux(lean_object*, uint8_t, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__25;
lean_object* lean_st_ref_take(lean_object*, lean_object*);
extern lean_object* l_Std_PersistentHashMap_insertAux___rarg___closed__3;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkCongrLemma___spec__6___closed__2;
@ -200,6 +199,7 @@ lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkCongrLemma___spec__8___la
lean_object* l_Std_PersistentHashMap_foldlMAux___at___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemmas____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_117____spec__5___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_addCongrLemmaEntry_match__1(lean_object*);
lean_object* l___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemmas____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_117____closed__2;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__28;
lean_object* l_Std_PersistentHashMap_insertAux___at_Lean_Meta_addCongrLemmaEntry___spec__3___lambda__1(lean_object*, lean_object*, size_t, size_t, size_t, size_t, lean_object*);
lean_object* lean_array_to_list(lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkCongrLemma___closed__1;
@ -325,9 +325,9 @@ lean_object* l_Lean_Meta_instInhabitedCongrLemmas;
uint8_t l_Lean_Meta_mkCongrLemma_onlyMVarsAt___lambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_find_x3f___at_Lean_Meta_CongrLemmas_get___spec__2(lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__26;
lean_object* l_Lean_Expr_withAppAux___at_Lean_Meta_mkCongrLemma___spec__11(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppFn(lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__26;
lean_object* l_Lean_Meta_congrExtension;
lean_object* l_Lean_mkLevelParam(lean_object*);
lean_object* l_Lean_Meta_mkCongrLemma_match__6___rarg(lean_object*, lean_object*);
@ -476,7 +476,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemma____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_21____closed__3;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__4;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__4;
x_3 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -567,7 +567,7 @@ x_15 = l___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemma
x_16 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_16, 0, x_14);
lean_ctor_set(x_16, 1, x_15);
x_17 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__4;
x_17 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__4;
x_18 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_18, 0, x_16);
lean_ctor_set(x_18, 1, x_17);
@ -648,15 +648,15 @@ lean_ctor_set(x_52, 1, x_17);
x_53 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_53, 0, x_52);
lean_ctor_set(x_53, 1, x_35);
x_54 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__26;
x_54 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__27;
x_55 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_55, 0, x_54);
lean_ctor_set(x_55, 1, x_53);
x_56 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__27;
x_56 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__28;
x_57 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_57, 0, x_55);
lean_ctor_set(x_57, 1, x_56);
x_58 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__25;
x_58 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__26;
x_59 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_59, 0, x_58);
lean_ctor_set(x_59, 1, x_57);
@ -690,15 +690,15 @@ lean_ctor_set(x_68, 1, x_17);
x_69 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_69, 0, x_68);
lean_ctor_set(x_69, 1, x_35);
x_70 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__26;
x_70 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__27;
x_71 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_71, 0, x_70);
lean_ctor_set(x_71, 1, x_69);
x_72 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__27;
x_72 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__28;
x_73 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_73, 0, x_71);
lean_ctor_set(x_73, 1, x_72);
x_74 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__25;
x_74 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__26;
x_75 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_75, 0, x_74);
lean_ctor_set(x_75, 1, x_73);
@ -1306,7 +1306,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemmas____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_117____closed__3;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__4;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__4;
x_3 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -1339,7 +1339,7 @@ static lean_object* _init_l___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__26;
x_1 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__27;
x_2 = l___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemmas____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_117____closed__6;
x_3 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -1352,7 +1352,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemmas____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_117____closed__7;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__27;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__28;
x_3 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -1363,7 +1363,7 @@ static lean_object* _init_l___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__25;
x_1 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__26;
x_2 = l___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemmas____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_117____closed__8;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -1425,15 +1425,15 @@ x_19 = l___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemma
x_20 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_20, 0, x_19);
lean_ctor_set(x_20, 1, x_18);
x_21 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__26;
x_21 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__27;
x_22 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_22, 0, x_21);
lean_ctor_set(x_22, 1, x_20);
x_23 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__27;
x_23 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__28;
x_24 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_24, 0, x_22);
lean_ctor_set(x_24, 1, x_23);
x_25 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__25;
x_25 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__26;
x_26 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_26, 0, x_25);
lean_ctor_set(x_26, 1, x_24);

321
stage0/stdlib/Lean/Meta/Tactic/Simp/Main.c generated
View file

@ -214,6 +214,7 @@ lean_object* l_Lean_Meta_withNewMCtxDepth___at_Lean_Meta_Simp_simp_tryCongrLemma
lean_object* l_Lean_Meta_Simp_initFn____x40_Lean_Meta_Tactic_Simp_Main___hyg_4_(lean_object*);
lean_object* l_Lean_Meta_Simp_post(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Simp_simp_simpArrow___closed__5;
extern lean_object* l_Lean_Meta_Simp_rewrite_getRHS___closed__3;
extern lean_object* l_Lean_instInhabitedExpr;
lean_object* l_Lean_Meta_Simp_simp_simpLambda_match__1___rarg(lean_object*, lean_object*, lean_object*);
size_t lean_usize_modn(size_t, lean_object*);
@ -239,7 +240,6 @@ lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_simp_congrDefault___sp
lean_object* l_Lean_Meta_Simp_simp_simpArrow___closed__15;
extern lean_object* l_Lean_KernelException_toMessageData___closed__3;
size_t lean_usize_of_nat(lean_object*);
extern lean_object* l_Lean_Meta_Simp_rewrite_getRHS___closed__2;
lean_object* l_Lean_isProjectionFn___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_reduceProjFn_x3f___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Simp_simp_withNewLemmas___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_instInhabitedParamInfo;
@ -7720,12 +7720,12 @@ x_10 = !lean_is_exclusive(x_3);
if (x_10 == 0)
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; uint8_t x_38; lean_object* x_39; lean_object* x_49; lean_object* x_50; lean_object* x_51; uint8_t x_52;
x_11 = lean_ctor_get(x_3, 3);
x_11 = lean_ctor_get(x_3, 4);
lean_dec(x_11);
lean_inc(x_1);
x_12 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_12, 0, x_1);
lean_ctor_set(x_3, 3, x_12);
lean_ctor_set(x_3, 4, x_12);
x_49 = lean_st_ref_get(x_8, x_9);
x_50 = lean_ctor_get(x_49, 0);
lean_inc(x_50);
@ -7909,132 +7909,135 @@ goto block_37;
}
else
{
lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; uint8_t x_88; lean_object* x_89; lean_object* x_99; lean_object* x_100; lean_object* x_101; uint8_t x_102;
lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; uint8_t x_89; lean_object* x_90; lean_object* x_100; lean_object* x_101; lean_object* x_102; uint8_t x_103;
x_61 = lean_ctor_get(x_3, 0);
x_62 = lean_ctor_get(x_3, 1);
x_63 = lean_ctor_get(x_3, 2);
x_64 = lean_ctor_get(x_3, 3);
lean_inc(x_64);
lean_inc(x_63);
lean_inc(x_62);
lean_inc(x_61);
lean_dec(x_3);
lean_inc(x_1);
x_64 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_64, 0, x_1);
x_65 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_65, 0, x_61);
lean_ctor_set(x_65, 1, x_62);
lean_ctor_set(x_65, 2, x_63);
lean_ctor_set(x_65, 3, x_64);
x_99 = lean_st_ref_get(x_8, x_9);
x_100 = lean_ctor_get(x_99, 0);
lean_inc(x_100);
x_101 = lean_ctor_get(x_100, 3);
x_65 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_65, 0, x_1);
x_66 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_66, 0, x_61);
lean_ctor_set(x_66, 1, x_62);
lean_ctor_set(x_66, 2, x_63);
lean_ctor_set(x_66, 3, x_64);
lean_ctor_set(x_66, 4, x_65);
x_100 = lean_st_ref_get(x_8, x_9);
x_101 = lean_ctor_get(x_100, 0);
lean_inc(x_101);
lean_dec(x_100);
x_102 = lean_ctor_get_uint8(x_101, sizeof(void*)*1);
x_102 = lean_ctor_get(x_101, 3);
lean_inc(x_102);
lean_dec(x_101);
if (x_102 == 0)
x_103 = lean_ctor_get_uint8(x_102, sizeof(void*)*1);
lean_dec(x_102);
if (x_103 == 0)
{
lean_object* x_103; uint8_t x_104;
x_103 = lean_ctor_get(x_99, 1);
lean_inc(x_103);
lean_dec(x_99);
x_104 = 0;
x_88 = x_104;
x_89 = x_103;
goto block_98;
lean_object* x_104; uint8_t x_105;
x_104 = lean_ctor_get(x_100, 1);
lean_inc(x_104);
lean_dec(x_100);
x_105 = 0;
x_89 = x_105;
x_90 = x_104;
goto block_99;
}
else
{
lean_object* x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109; uint8_t x_110;
x_105 = lean_ctor_get(x_99, 1);
lean_inc(x_105);
lean_dec(x_99);
x_106 = l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_synthesizeArgs___spec__3___closed__2;
x_107 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Meta_Simp_simp_simpForall___spec__4(x_106, x_2, x_65, x_4, x_5, x_6, x_7, x_8, x_105);
x_108 = lean_ctor_get(x_107, 0);
lean_inc(x_108);
x_109 = lean_ctor_get(x_107, 1);
lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109; lean_object* x_110; uint8_t x_111;
x_106 = lean_ctor_get(x_100, 1);
lean_inc(x_106);
lean_dec(x_100);
x_107 = l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_synthesizeArgs___spec__3___closed__2;
x_108 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Meta_Simp_simp_simpForall___spec__4(x_107, x_2, x_66, x_4, x_5, x_6, x_7, x_8, x_106);
x_109 = lean_ctor_get(x_108, 0);
lean_inc(x_109);
lean_dec(x_107);
x_110 = lean_unbox(x_108);
x_110 = lean_ctor_get(x_108, 1);
lean_inc(x_110);
lean_dec(x_108);
x_88 = x_110;
x_89 = x_109;
goto block_98;
x_111 = lean_unbox(x_109);
lean_dec(x_109);
x_89 = x_111;
x_90 = x_110;
goto block_99;
}
block_87:
block_88:
{
uint8_t x_67;
x_67 = l_Lean_Expr_isArrow(x_1);
if (x_67 == 0)
uint8_t x_68;
x_68 = l_Lean_Expr_isArrow(x_1);
if (x_68 == 0)
{
lean_object* x_68;
lean_object* x_69;
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_1);
x_68 = l_Lean_Meta_isProp(x_1, x_5, x_6, x_7, x_8, x_66);
if (lean_obj_tag(x_68) == 0)
x_69 = l_Lean_Meta_isProp(x_1, x_5, x_6, x_7, x_8, x_67);
if (lean_obj_tag(x_69) == 0)
{
lean_object* x_69; uint8_t x_70;
x_69 = lean_ctor_get(x_68, 0);
lean_inc(x_69);
x_70 = lean_unbox(x_69);
lean_dec(x_69);
if (x_70 == 0)
lean_object* x_70; uint8_t x_71;
x_70 = lean_ctor_get(x_69, 0);
lean_inc(x_70);
x_71 = lean_unbox(x_70);
lean_dec(x_70);
if (x_71 == 0)
{
lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75;
lean_dec(x_65);
lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76;
lean_dec(x_66);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
x_71 = lean_ctor_get(x_68, 1);
lean_inc(x_71);
if (lean_is_exclusive(x_68)) {
lean_ctor_release(x_68, 0);
lean_ctor_release(x_68, 1);
x_72 = x_68;
x_72 = lean_ctor_get(x_69, 1);
lean_inc(x_72);
if (lean_is_exclusive(x_69)) {
lean_ctor_release(x_69, 0);
lean_ctor_release(x_69, 1);
x_73 = x_69;
} else {
lean_dec_ref(x_68);
x_72 = lean_box(0);
lean_dec_ref(x_69);
x_73 = lean_box(0);
}
x_73 = lean_box(0);
x_74 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_74, 0, x_1);
lean_ctor_set(x_74, 1, x_73);
if (lean_is_scalar(x_72)) {
x_75 = lean_alloc_ctor(0, 2, 0);
x_74 = lean_box(0);
x_75 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_75, 0, x_1);
lean_ctor_set(x_75, 1, x_74);
if (lean_is_scalar(x_73)) {
x_76 = lean_alloc_ctor(0, 2, 0);
} else {
x_75 = x_72;
x_76 = x_73;
}
lean_ctor_set(x_75, 0, x_74);
lean_ctor_set(x_75, 1, x_71);
return x_75;
lean_ctor_set(x_76, 0, x_75);
lean_ctor_set(x_76, 1, x_72);
return x_76;
}
else
{
lean_object* x_76; lean_object* x_77; uint8_t x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81;
x_76 = lean_ctor_get(x_68, 1);
lean_inc(x_76);
lean_dec(x_68);
x_77 = l_Lean_Expr_bindingName_x21(x_1);
x_78 = l_Lean_Expr_bindingInfo_x21(x_1);
x_79 = l_Lean_Expr_bindingDomain_x21(x_1);
x_80 = lean_alloc_closure((void*)(l_Lean_Meta_Simp_simp_simpForall___lambda__2___boxed), 10, 1);
lean_closure_set(x_80, 0, x_1);
x_81 = l_Lean_Meta_withLocalDecl___at_Lean_Meta_Simp_simp_simpForall___spec__2___rarg(x_77, x_78, x_79, x_80, x_2, x_65, x_4, x_5, x_6, x_7, x_8, x_76);
return x_81;
lean_object* x_77; lean_object* x_78; uint8_t x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82;
x_77 = lean_ctor_get(x_69, 1);
lean_inc(x_77);
lean_dec(x_69);
x_78 = l_Lean_Expr_bindingName_x21(x_1);
x_79 = l_Lean_Expr_bindingInfo_x21(x_1);
x_80 = l_Lean_Expr_bindingDomain_x21(x_1);
x_81 = lean_alloc_closure((void*)(l_Lean_Meta_Simp_simp_simpForall___lambda__2___boxed), 10, 1);
lean_closure_set(x_81, 0, x_1);
x_82 = l_Lean_Meta_withLocalDecl___at_Lean_Meta_Simp_simp_simpForall___spec__2___rarg(x_78, x_79, x_80, x_81, x_2, x_66, x_4, x_5, x_6, x_7, x_8, x_77);
return x_82;
}
}
else
{
lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85;
lean_dec(x_65);
lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86;
lean_dec(x_66);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
@ -8042,63 +8045,63 @@ lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
x_82 = lean_ctor_get(x_68, 0);
lean_inc(x_82);
x_83 = lean_ctor_get(x_68, 1);
x_83 = lean_ctor_get(x_69, 0);
lean_inc(x_83);
if (lean_is_exclusive(x_68)) {
lean_ctor_release(x_68, 0);
lean_ctor_release(x_68, 1);
x_84 = x_68;
x_84 = lean_ctor_get(x_69, 1);
lean_inc(x_84);
if (lean_is_exclusive(x_69)) {
lean_ctor_release(x_69, 0);
lean_ctor_release(x_69, 1);
x_85 = x_69;
} else {
lean_dec_ref(x_68);
x_84 = lean_box(0);
lean_dec_ref(x_69);
x_85 = lean_box(0);
}
if (lean_is_scalar(x_84)) {
x_85 = lean_alloc_ctor(1, 2, 0);
if (lean_is_scalar(x_85)) {
x_86 = lean_alloc_ctor(1, 2, 0);
} else {
x_85 = x_84;
x_86 = x_85;
}
lean_ctor_set(x_85, 0, x_82);
lean_ctor_set(x_85, 1, x_83);
return x_85;
}
}
else
{
lean_object* x_86;
x_86 = l_Lean_Meta_Simp_simp_simpArrow(x_1, x_2, x_65, x_4, x_5, x_6, x_7, x_8, x_66);
lean_ctor_set(x_86, 0, x_83);
lean_ctor_set(x_86, 1, x_84);
return x_86;
}
}
block_98:
else
{
if (x_88 == 0)
lean_object* x_87;
x_87 = l_Lean_Meta_Simp_simp_simpArrow(x_1, x_2, x_66, x_4, x_5, x_6, x_7, x_8, x_67);
return x_87;
}
}
block_99:
{
x_66 = x_89;
goto block_87;
if (x_89 == 0)
{
x_67 = x_90;
goto block_88;
}
else
{
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_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_inc(x_1);
x_90 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_90, 0, x_1);
x_91 = l_Lean_Meta_Simp_simp_simpForall___closed__2;
x_92 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_92, 0, x_91);
lean_ctor_set(x_92, 1, x_90);
x_93 = l_Lean_KernelException_toMessageData___closed__15;
x_94 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_94, 0, x_92);
lean_ctor_set(x_94, 1, x_93);
x_95 = l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_synthesizeArgs___spec__3___closed__2;
x_96 = l_Lean_addTrace___at_Lean_Meta_Simp_simp_simpForall___spec__3(x_95, x_94, x_2, x_65, x_4, x_5, x_6, x_7, x_8, x_89);
x_97 = lean_ctor_get(x_96, 1);
lean_inc(x_97);
lean_dec(x_96);
x_66 = x_97;
goto block_87;
x_91 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_91, 0, x_1);
x_92 = l_Lean_Meta_Simp_simp_simpForall___closed__2;
x_93 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_93, 0, x_92);
lean_ctor_set(x_93, 1, x_91);
x_94 = l_Lean_KernelException_toMessageData___closed__15;
x_95 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_95, 0, x_93);
lean_ctor_set(x_95, 1, x_94);
x_96 = l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_synthesizeArgs___spec__3___closed__2;
x_97 = l_Lean_addTrace___at_Lean_Meta_Simp_simp_simpForall___spec__3(x_96, x_95, x_2, x_66, x_4, x_5, x_6, x_7, x_8, x_90);
x_98 = lean_ctor_get(x_97, 1);
lean_inc(x_98);
lean_dec(x_97);
x_67 = x_98;
goto block_88;
}
}
}
@ -10308,37 +10311,40 @@ x_10 = !lean_is_exclusive(x_3);
if (x_10 == 0)
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_11 = lean_ctor_get(x_3, 3);
x_11 = lean_ctor_get(x_3, 4);
lean_dec(x_11);
lean_inc(x_1);
x_12 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_12, 0, x_1);
lean_ctor_set(x_3, 3, x_12);
lean_ctor_set(x_3, 4, x_12);
x_13 = l_Lean_Meta_Simp_simp_simpLambda___closed__1;
x_14 = l_Lean_Meta_lambdaTelescope___at_Lean_Meta_Simp_simp_simpLambda___spec__4___rarg(x_1, x_13, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
return x_14;
}
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_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;
x_15 = lean_ctor_get(x_3, 0);
x_16 = lean_ctor_get(x_3, 1);
x_17 = lean_ctor_get(x_3, 2);
x_18 = lean_ctor_get(x_3, 3);
lean_inc(x_18);
lean_inc(x_17);
lean_inc(x_16);
lean_inc(x_15);
lean_dec(x_3);
lean_inc(x_1);
x_18 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_18, 0, x_1);
x_19 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_19, 0, x_15);
lean_ctor_set(x_19, 1, x_16);
lean_ctor_set(x_19, 2, x_17);
lean_ctor_set(x_19, 3, x_18);
x_20 = l_Lean_Meta_Simp_simp_simpLambda___closed__1;
x_21 = l_Lean_Meta_lambdaTelescope___at_Lean_Meta_Simp_simp_simpLambda___spec__4___rarg(x_1, x_20, x_2, x_19, x_4, x_5, x_6, x_7, x_8, x_9);
return x_21;
x_19 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_19, 0, x_1);
x_20 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_20, 0, x_15);
lean_ctor_set(x_20, 1, x_16);
lean_ctor_set(x_20, 2, x_17);
lean_ctor_set(x_20, 3, x_18);
lean_ctor_set(x_20, 4, x_19);
x_21 = l_Lean_Meta_Simp_simp_simpLambda___closed__1;
x_22 = l_Lean_Meta_lambdaTelescope___at_Lean_Meta_Simp_simp_simpLambda___spec__4___rarg(x_1, x_21, x_2, x_20, x_4, x_5, x_6, x_7, x_8, x_9);
return x_22;
}
}
}
@ -11519,35 +11525,38 @@ x_16 = !lean_is_exclusive(x_3);
if (x_16 == 0)
{
lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_17 = lean_ctor_get(x_3, 3);
x_17 = lean_ctor_get(x_3, 4);
lean_dec(x_17);
lean_inc(x_1);
x_18 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_18, 0, x_1);
lean_ctor_set(x_3, 3, x_18);
lean_ctor_set(x_3, 4, x_18);
x_19 = l_Lean_Expr_withAppAux___at_Lean_Meta_Simp_simp_congrDefault___spec__2(x_1, x_13, x_15, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
return x_19;
}
else
{
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_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_20 = lean_ctor_get(x_3, 0);
x_21 = lean_ctor_get(x_3, 1);
x_22 = lean_ctor_get(x_3, 2);
x_23 = lean_ctor_get(x_3, 3);
lean_inc(x_23);
lean_inc(x_22);
lean_inc(x_21);
lean_inc(x_20);
lean_dec(x_3);
lean_inc(x_1);
x_23 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_23, 0, x_1);
x_24 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_24, 0, x_20);
lean_ctor_set(x_24, 1, x_21);
lean_ctor_set(x_24, 2, x_22);
lean_ctor_set(x_24, 3, x_23);
x_25 = l_Lean_Expr_withAppAux___at_Lean_Meta_Simp_simp_congrDefault___spec__2(x_1, x_13, x_15, x_2, x_24, x_4, x_5, x_6, x_7, x_8, x_9);
return x_25;
x_24 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_24, 0, x_1);
x_25 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_25, 0, x_20);
lean_ctor_set(x_25, 1, x_21);
lean_ctor_set(x_25, 2, x_22);
lean_ctor_set(x_25, 3, x_23);
lean_ctor_set(x_25, 4, x_24);
x_26 = l_Lean_Expr_withAppAux___at_Lean_Meta_Simp_simp_congrDefault___spec__2(x_1, x_13, x_15, x_2, x_25, x_4, x_5, x_6, x_7, x_8, x_9);
return x_26;
}
}
}
@ -14727,7 +14736,7 @@ x_12 = lean_ctor_get(x_10, 0);
x_13 = lean_ctor_get(x_10, 1);
x_14 = lean_ctor_get(x_12, 0);
lean_inc(x_14);
x_15 = l_Lean_Meta_Simp_rewrite_getRHS___closed__2;
x_15 = l_Lean_Meta_Simp_rewrite_getRHS___closed__3;
x_16 = l_Lean_Expr_isConstOf(x_14, x_15);
lean_dec(x_14);
if (x_16 == 0)
@ -14860,7 +14869,7 @@ lean_inc(x_41);
lean_dec(x_10);
x_43 = lean_ctor_get(x_41, 0);
lean_inc(x_43);
x_44 = l_Lean_Meta_Simp_rewrite_getRHS___closed__2;
x_44 = l_Lean_Meta_Simp_rewrite_getRHS___closed__3;
x_45 = l_Lean_Expr_isConstOf(x_43, x_44);
lean_dec(x_43);
if (x_45 == 0)

4651
stage0/stdlib/Lean/Meta/Tactic/Simp/Rewrite.c generated
View file

File diff suppressed because it is too large Load diff

2928
stage0/stdlib/Lean/Meta/Tactic/Simp/SimpLemmas.c generated
View file

File diff suppressed because it is too large Load diff

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

@ -19,6 +19,7 @@ lean_object* l_Lean_Meta_Simp_State_cache___default;
lean_object* l_Lean_Meta_Simp_Methods_pre___default(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Simp_withSimpLemmas(lean_object*);
lean_object* l_Lean_Meta_Simp_Step_result_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Simp_Context_toUnfold___default;
lean_object* l_Lean_Meta_Simp_getCongrLemmas___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_get(lean_object*, lean_object*);
lean_object* l_Lean_Meta_Simp_getCongrLemmas(lean_object*);
@ -51,6 +52,7 @@ lean_object* l_Lean_Meta_Simp_State_cache___default___closed__1;
lean_object* l_Lean_Meta_Simp_instInhabitedMethods___closed__1;
lean_object* l_Lean_Meta_Simp_instInhabitedResult___closed__1;
lean_object* l_Lean_Meta_Simp_getSimpLemmas___boxed(lean_object*);
extern lean_object* l_Lean_NameSet_empty;
lean_object* l_Lean_Meta_Simp_getConfig___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Simp_instInhabitedMethods___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Simp_Methods_pre___default___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -95,6 +97,14 @@ x_1 = l_Lean_Meta_Simp_instInhabitedResult___closed__1;
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Simp_Context_toUnfold___default() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_NameSet_empty;
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Simp_Context_parent_x3f___default() {
_start:
{
@ -472,33 +482,36 @@ x_11 = !lean_is_exclusive(x_4);
if (x_11 == 0)
{
lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_12 = lean_ctor_get(x_4, 3);
x_12 = lean_ctor_get(x_4, 4);
lean_dec(x_12);
x_13 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_13, 0, x_1);
lean_ctor_set(x_4, 3, x_13);
lean_ctor_set(x_4, 4, x_13);
x_14 = lean_apply_8(x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
return x_14;
}
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_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;
x_15 = lean_ctor_get(x_4, 0);
x_16 = lean_ctor_get(x_4, 1);
x_17 = lean_ctor_get(x_4, 2);
x_18 = lean_ctor_get(x_4, 3);
lean_inc(x_18);
lean_inc(x_17);
lean_inc(x_16);
lean_inc(x_15);
lean_dec(x_4);
x_18 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_18, 0, x_1);
x_19 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_19, 0, x_15);
lean_ctor_set(x_19, 1, x_16);
lean_ctor_set(x_19, 2, x_17);
lean_ctor_set(x_19, 3, x_18);
x_20 = lean_apply_8(x_2, x_3, x_19, x_5, x_6, x_7, x_8, x_9, x_10);
return x_20;
x_19 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_19, 0, x_1);
x_20 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_20, 0, x_15);
lean_ctor_set(x_20, 1, x_16);
lean_ctor_set(x_20, 2, x_17);
lean_ctor_set(x_20, 3, x_18);
lean_ctor_set(x_20, 4, x_19);
x_21 = lean_apply_8(x_2, x_3, x_20, x_5, x_6, x_7, x_8, x_9, x_10);
return x_21;
}
}
}
@ -810,295 +823,302 @@ return x_69;
}
else
{
lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74;
lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75;
x_70 = lean_ctor_get(x_4, 0);
x_71 = lean_ctor_get(x_4, 2);
x_72 = lean_ctor_get(x_4, 3);
x_73 = lean_ctor_get(x_4, 4);
lean_inc(x_73);
lean_inc(x_72);
lean_inc(x_71);
lean_inc(x_70);
lean_dec(x_4);
x_73 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_73, 0, x_70);
lean_ctor_set(x_73, 1, x_1);
lean_ctor_set(x_73, 2, x_71);
lean_ctor_set(x_73, 3, x_72);
x_74 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_74, 0, x_70);
lean_ctor_set(x_74, 1, x_1);
lean_ctor_set(x_74, 2, x_71);
lean_ctor_set(x_74, 3, x_72);
lean_ctor_set(x_74, 4, x_73);
lean_inc(x_9);
lean_inc(x_5);
x_74 = lean_apply_8(x_2, x_3, x_73, x_5, x_6, x_7, x_8, x_9, x_26);
if (lean_obj_tag(x_74) == 0)
x_75 = lean_apply_8(x_2, x_3, x_74, x_5, x_6, x_7, x_8, x_9, x_26);
if (lean_obj_tag(x_75) == 0)
{
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_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_88;
x_75 = lean_ctor_get(x_74, 0);
lean_inc(x_75);
x_76 = lean_ctor_get(x_74, 1);
lean_object* x_76; lean_object* x_77; lean_object* 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_88; lean_object* x_89;
x_76 = lean_ctor_get(x_75, 0);
lean_inc(x_76);
lean_dec(x_74);
x_77 = lean_st_ref_get(x_9, x_76);
x_77 = lean_ctor_get(x_75, 1);
lean_inc(x_77);
lean_dec(x_75);
x_78 = lean_st_ref_get(x_9, x_77);
lean_dec(x_9);
x_78 = lean_ctor_get(x_77, 1);
lean_inc(x_78);
lean_dec(x_77);
x_79 = lean_st_ref_take(x_5, x_78);
x_80 = lean_ctor_get(x_79, 0);
lean_inc(x_80);
x_81 = lean_ctor_get(x_79, 1);
x_79 = lean_ctor_get(x_78, 1);
lean_inc(x_79);
lean_dec(x_78);
x_80 = lean_st_ref_take(x_5, x_79);
x_81 = lean_ctor_get(x_80, 0);
lean_inc(x_81);
lean_dec(x_79);
x_82 = lean_ctor_get(x_80, 1);
lean_inc(x_82);
if (lean_is_exclusive(x_80)) {
lean_ctor_release(x_80, 0);
lean_ctor_release(x_80, 1);
x_83 = x_80;
lean_dec(x_80);
x_83 = lean_ctor_get(x_81, 1);
lean_inc(x_83);
if (lean_is_exclusive(x_81)) {
lean_ctor_release(x_81, 0);
lean_ctor_release(x_81, 1);
x_84 = x_81;
} else {
lean_dec_ref(x_80);
x_83 = lean_box(0);
lean_dec_ref(x_81);
x_84 = lean_box(0);
}
if (lean_is_scalar(x_83)) {
x_84 = lean_alloc_ctor(0, 2, 0);
if (lean_is_scalar(x_84)) {
x_85 = lean_alloc_ctor(0, 2, 0);
} else {
x_84 = x_83;
x_85 = x_84;
}
lean_ctor_set(x_84, 0, x_16);
lean_ctor_set(x_84, 1, x_82);
x_85 = lean_st_ref_set(x_5, x_84, x_81);
lean_ctor_set(x_85, 0, x_16);
lean_ctor_set(x_85, 1, x_83);
x_86 = lean_st_ref_set(x_5, x_85, x_82);
lean_dec(x_5);
x_86 = lean_ctor_get(x_85, 1);
lean_inc(x_86);
if (lean_is_exclusive(x_85)) {
lean_ctor_release(x_85, 0);
lean_ctor_release(x_85, 1);
x_87 = x_85;
x_87 = lean_ctor_get(x_86, 1);
lean_inc(x_87);
if (lean_is_exclusive(x_86)) {
lean_ctor_release(x_86, 0);
lean_ctor_release(x_86, 1);
x_88 = x_86;
} else {
lean_dec_ref(x_85);
x_87 = lean_box(0);
lean_dec_ref(x_86);
x_88 = lean_box(0);
}
if (lean_is_scalar(x_87)) {
x_88 = lean_alloc_ctor(0, 2, 0);
if (lean_is_scalar(x_88)) {
x_89 = lean_alloc_ctor(0, 2, 0);
} else {
x_88 = x_87;
x_89 = x_88;
}
lean_ctor_set(x_88, 0, x_75);
lean_ctor_set(x_88, 1, x_86);
return x_88;
lean_ctor_set(x_89, 0, x_76);
lean_ctor_set(x_89, 1, x_87);
return x_89;
}
else
{
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; lean_object* x_100; lean_object* x_101; lean_object* x_102;
x_89 = lean_ctor_get(x_74, 0);
lean_inc(x_89);
x_90 = lean_ctor_get(x_74, 1);
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; lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103;
x_90 = lean_ctor_get(x_75, 0);
lean_inc(x_90);
lean_dec(x_74);
x_91 = lean_st_ref_get(x_9, x_90);
x_91 = lean_ctor_get(x_75, 1);
lean_inc(x_91);
lean_dec(x_75);
x_92 = lean_st_ref_get(x_9, x_91);
lean_dec(x_9);
x_92 = lean_ctor_get(x_91, 1);
lean_inc(x_92);
lean_dec(x_91);
x_93 = lean_st_ref_take(x_5, x_92);
x_94 = lean_ctor_get(x_93, 0);
lean_inc(x_94);
x_95 = lean_ctor_get(x_93, 1);
x_93 = lean_ctor_get(x_92, 1);
lean_inc(x_93);
lean_dec(x_92);
x_94 = lean_st_ref_take(x_5, x_93);
x_95 = lean_ctor_get(x_94, 0);
lean_inc(x_95);
lean_dec(x_93);
x_96 = lean_ctor_get(x_94, 1);
lean_inc(x_96);
if (lean_is_exclusive(x_94)) {
lean_ctor_release(x_94, 0);
lean_ctor_release(x_94, 1);
x_97 = x_94;
lean_dec(x_94);
x_97 = lean_ctor_get(x_95, 1);
lean_inc(x_97);
if (lean_is_exclusive(x_95)) {
lean_ctor_release(x_95, 0);
lean_ctor_release(x_95, 1);
x_98 = x_95;
} else {
lean_dec_ref(x_94);
x_97 = lean_box(0);
lean_dec_ref(x_95);
x_98 = lean_box(0);
}
if (lean_is_scalar(x_97)) {
x_98 = lean_alloc_ctor(0, 2, 0);
if (lean_is_scalar(x_98)) {
x_99 = lean_alloc_ctor(0, 2, 0);
} else {
x_98 = x_97;
x_99 = x_98;
}
lean_ctor_set(x_98, 0, x_16);
lean_ctor_set(x_98, 1, x_96);
x_99 = lean_st_ref_set(x_5, x_98, x_95);
lean_ctor_set(x_99, 0, x_16);
lean_ctor_set(x_99, 1, x_97);
x_100 = lean_st_ref_set(x_5, x_99, x_96);
lean_dec(x_5);
x_100 = lean_ctor_get(x_99, 1);
lean_inc(x_100);
if (lean_is_exclusive(x_99)) {
lean_ctor_release(x_99, 0);
lean_ctor_release(x_99, 1);
x_101 = x_99;
x_101 = lean_ctor_get(x_100, 1);
lean_inc(x_101);
if (lean_is_exclusive(x_100)) {
lean_ctor_release(x_100, 0);
lean_ctor_release(x_100, 1);
x_102 = x_100;
} else {
lean_dec_ref(x_99);
x_101 = lean_box(0);
lean_dec_ref(x_100);
x_102 = lean_box(0);
}
if (lean_is_scalar(x_101)) {
x_102 = lean_alloc_ctor(1, 2, 0);
if (lean_is_scalar(x_102)) {
x_103 = lean_alloc_ctor(1, 2, 0);
} else {
x_102 = x_101;
lean_ctor_set_tag(x_102, 1);
x_103 = x_102;
lean_ctor_set_tag(x_103, 1);
}
lean_ctor_set(x_102, 0, x_89);
lean_ctor_set(x_102, 1, x_100);
return x_102;
lean_ctor_set(x_103, 0, x_90);
lean_ctor_set(x_103, 1, x_101);
return x_103;
}
}
}
else
{
lean_object* x_103; lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113;
x_103 = lean_ctor_get(x_20, 1);
lean_inc(x_103);
lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113; lean_object* x_114; lean_object* x_115;
x_104 = lean_ctor_get(x_20, 1);
lean_inc(x_104);
lean_dec(x_20);
x_104 = l_Std_HashMap_instInhabitedHashMap___closed__1;
x_105 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_105, 0, x_104);
lean_ctor_set(x_105, 1, x_103);
x_106 = lean_st_ref_set(x_5, x_105, x_21);
x_107 = lean_ctor_get(x_106, 1);
lean_inc(x_107);
lean_dec(x_106);
x_108 = lean_ctor_get(x_4, 0);
x_105 = l_Std_HashMap_instInhabitedHashMap___closed__1;
x_106 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_106, 0, x_105);
lean_ctor_set(x_106, 1, x_104);
x_107 = lean_st_ref_set(x_5, x_106, x_21);
x_108 = lean_ctor_get(x_107, 1);
lean_inc(x_108);
x_109 = lean_ctor_get(x_4, 2);
lean_dec(x_107);
x_109 = lean_ctor_get(x_4, 0);
lean_inc(x_109);
x_110 = lean_ctor_get(x_4, 3);
x_110 = lean_ctor_get(x_4, 2);
lean_inc(x_110);
x_111 = lean_ctor_get(x_4, 3);
lean_inc(x_111);
x_112 = lean_ctor_get(x_4, 4);
lean_inc(x_112);
if (lean_is_exclusive(x_4)) {
lean_ctor_release(x_4, 0);
lean_ctor_release(x_4, 1);
lean_ctor_release(x_4, 2);
lean_ctor_release(x_4, 3);
x_111 = x_4;
lean_ctor_release(x_4, 4);
x_113 = x_4;
} else {
lean_dec_ref(x_4);
x_111 = lean_box(0);
x_113 = lean_box(0);
}
if (lean_is_scalar(x_111)) {
x_112 = lean_alloc_ctor(0, 4, 0);
if (lean_is_scalar(x_113)) {
x_114 = lean_alloc_ctor(0, 5, 0);
} else {
x_112 = x_111;
x_114 = x_113;
}
lean_ctor_set(x_112, 0, x_108);
lean_ctor_set(x_112, 1, x_1);
lean_ctor_set(x_112, 2, x_109);
lean_ctor_set(x_112, 3, x_110);
lean_ctor_set(x_114, 0, x_109);
lean_ctor_set(x_114, 1, x_1);
lean_ctor_set(x_114, 2, x_110);
lean_ctor_set(x_114, 3, x_111);
lean_ctor_set(x_114, 4, x_112);
lean_inc(x_9);
lean_inc(x_5);
x_113 = lean_apply_8(x_2, x_3, x_112, x_5, x_6, x_7, x_8, x_9, x_107);
if (lean_obj_tag(x_113) == 0)
x_115 = lean_apply_8(x_2, x_3, x_114, x_5, x_6, x_7, x_8, x_9, x_108);
if (lean_obj_tag(x_115) == 0)
{
lean_object* x_114; lean_object* x_115; lean_object* x_116; lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* 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;
x_114 = lean_ctor_get(x_113, 0);
lean_inc(x_114);
x_115 = lean_ctor_get(x_113, 1);
lean_inc(x_115);
lean_dec(x_113);
x_116 = lean_st_ref_get(x_9, x_115);
lean_dec(x_9);
x_117 = lean_ctor_get(x_116, 1);
lean_object* x_116; lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* 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;
x_116 = lean_ctor_get(x_115, 0);
lean_inc(x_116);
x_117 = lean_ctor_get(x_115, 1);
lean_inc(x_117);
lean_dec(x_116);
x_118 = lean_st_ref_take(x_5, x_117);
x_119 = lean_ctor_get(x_118, 0);
lean_dec(x_115);
x_118 = lean_st_ref_get(x_9, x_117);
lean_dec(x_9);
x_119 = lean_ctor_get(x_118, 1);
lean_inc(x_119);
x_120 = lean_ctor_get(x_118, 1);
lean_inc(x_120);
lean_dec(x_118);
x_121 = lean_ctor_get(x_119, 1);
x_120 = lean_st_ref_take(x_5, x_119);
x_121 = lean_ctor_get(x_120, 0);
lean_inc(x_121);
if (lean_is_exclusive(x_119)) {
lean_ctor_release(x_119, 0);
lean_ctor_release(x_119, 1);
x_122 = x_119;
x_122 = lean_ctor_get(x_120, 1);
lean_inc(x_122);
lean_dec(x_120);
x_123 = lean_ctor_get(x_121, 1);
lean_inc(x_123);
if (lean_is_exclusive(x_121)) {
lean_ctor_release(x_121, 0);
lean_ctor_release(x_121, 1);
x_124 = x_121;
} else {
lean_dec_ref(x_119);
x_122 = lean_box(0);
lean_dec_ref(x_121);
x_124 = lean_box(0);
}
if (lean_is_scalar(x_122)) {
x_123 = lean_alloc_ctor(0, 2, 0);
if (lean_is_scalar(x_124)) {
x_125 = lean_alloc_ctor(0, 2, 0);
} else {
x_123 = x_122;
x_125 = x_124;
}
lean_ctor_set(x_123, 0, x_16);
lean_ctor_set(x_123, 1, x_121);
x_124 = lean_st_ref_set(x_5, x_123, x_120);
lean_ctor_set(x_125, 0, x_16);
lean_ctor_set(x_125, 1, x_123);
x_126 = lean_st_ref_set(x_5, x_125, x_122);
lean_dec(x_5);
x_125 = lean_ctor_get(x_124, 1);
lean_inc(x_125);
if (lean_is_exclusive(x_124)) {
lean_ctor_release(x_124, 0);
lean_ctor_release(x_124, 1);
x_126 = x_124;
x_127 = lean_ctor_get(x_126, 1);
lean_inc(x_127);
if (lean_is_exclusive(x_126)) {
lean_ctor_release(x_126, 0);
lean_ctor_release(x_126, 1);
x_128 = x_126;
} else {
lean_dec_ref(x_124);
x_126 = lean_box(0);
lean_dec_ref(x_126);
x_128 = lean_box(0);
}
if (lean_is_scalar(x_126)) {
x_127 = lean_alloc_ctor(0, 2, 0);
if (lean_is_scalar(x_128)) {
x_129 = lean_alloc_ctor(0, 2, 0);
} else {
x_127 = x_126;
x_129 = x_128;
}
lean_ctor_set(x_127, 0, x_114);
lean_ctor_set(x_127, 1, x_125);
return x_127;
lean_ctor_set(x_129, 0, x_116);
lean_ctor_set(x_129, 1, x_127);
return x_129;
}
else
{
lean_object* x_128; lean_object* x_129; lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; lean_object* x_134; lean_object* x_135; lean_object* x_136; lean_object* x_137; lean_object* x_138; lean_object* x_139; lean_object* x_140; lean_object* x_141;
x_128 = lean_ctor_get(x_113, 0);
lean_inc(x_128);
x_129 = lean_ctor_get(x_113, 1);
lean_inc(x_129);
lean_dec(x_113);
x_130 = lean_st_ref_get(x_9, x_129);
lean_dec(x_9);
x_131 = lean_ctor_get(x_130, 1);
lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; lean_object* x_134; lean_object* x_135; lean_object* x_136; lean_object* x_137; lean_object* x_138; lean_object* x_139; lean_object* x_140; lean_object* x_141; lean_object* x_142; lean_object* x_143;
x_130 = lean_ctor_get(x_115, 0);
lean_inc(x_130);
x_131 = lean_ctor_get(x_115, 1);
lean_inc(x_131);
lean_dec(x_130);
x_132 = lean_st_ref_take(x_5, x_131);
x_133 = lean_ctor_get(x_132, 0);
lean_dec(x_115);
x_132 = lean_st_ref_get(x_9, x_131);
lean_dec(x_9);
x_133 = lean_ctor_get(x_132, 1);
lean_inc(x_133);
x_134 = lean_ctor_get(x_132, 1);
lean_inc(x_134);
lean_dec(x_132);
x_135 = lean_ctor_get(x_133, 1);
x_134 = lean_st_ref_take(x_5, x_133);
x_135 = lean_ctor_get(x_134, 0);
lean_inc(x_135);
if (lean_is_exclusive(x_133)) {
lean_ctor_release(x_133, 0);
lean_ctor_release(x_133, 1);
x_136 = x_133;
x_136 = lean_ctor_get(x_134, 1);
lean_inc(x_136);
lean_dec(x_134);
x_137 = lean_ctor_get(x_135, 1);
lean_inc(x_137);
if (lean_is_exclusive(x_135)) {
lean_ctor_release(x_135, 0);
lean_ctor_release(x_135, 1);
x_138 = x_135;
} else {
lean_dec_ref(x_133);
x_136 = lean_box(0);
lean_dec_ref(x_135);
x_138 = lean_box(0);
}
if (lean_is_scalar(x_136)) {
x_137 = lean_alloc_ctor(0, 2, 0);
if (lean_is_scalar(x_138)) {
x_139 = lean_alloc_ctor(0, 2, 0);
} else {
x_137 = x_136;
x_139 = x_138;
}
lean_ctor_set(x_137, 0, x_16);
lean_ctor_set(x_137, 1, x_135);
x_138 = lean_st_ref_set(x_5, x_137, x_134);
lean_ctor_set(x_139, 0, x_16);
lean_ctor_set(x_139, 1, x_137);
x_140 = lean_st_ref_set(x_5, x_139, x_136);
lean_dec(x_5);
x_139 = lean_ctor_get(x_138, 1);
lean_inc(x_139);
if (lean_is_exclusive(x_138)) {
lean_ctor_release(x_138, 0);
lean_ctor_release(x_138, 1);
x_140 = x_138;
x_141 = lean_ctor_get(x_140, 1);
lean_inc(x_141);
if (lean_is_exclusive(x_140)) {
lean_ctor_release(x_140, 0);
lean_ctor_release(x_140, 1);
x_142 = x_140;
} else {
lean_dec_ref(x_138);
x_140 = lean_box(0);
lean_dec_ref(x_140);
x_142 = lean_box(0);
}
if (lean_is_scalar(x_140)) {
x_141 = lean_alloc_ctor(1, 2, 0);
if (lean_is_scalar(x_142)) {
x_143 = lean_alloc_ctor(1, 2, 0);
} else {
x_141 = x_140;
lean_ctor_set_tag(x_141, 1);
x_143 = x_142;
lean_ctor_set_tag(x_143, 1);
}
lean_ctor_set(x_141, 0, x_128);
lean_ctor_set(x_141, 1, x_139);
return x_141;
lean_ctor_set(x_143, 0, x_130);
lean_ctor_set(x_143, 1, x_141);
return x_143;
}
}
}
@ -1138,6 +1158,8 @@ l_Lean_Meta_Simp_instInhabitedResult___closed__1 = _init_l_Lean_Meta_Simp_instIn
lean_mark_persistent(l_Lean_Meta_Simp_instInhabitedResult___closed__1);
l_Lean_Meta_Simp_instInhabitedResult = _init_l_Lean_Meta_Simp_instInhabitedResult();
lean_mark_persistent(l_Lean_Meta_Simp_instInhabitedResult);
l_Lean_Meta_Simp_Context_toUnfold___default = _init_l_Lean_Meta_Simp_Context_toUnfold___default();
lean_mark_persistent(l_Lean_Meta_Simp_Context_toUnfold___default);
l_Lean_Meta_Simp_Context_parent_x3f___default = _init_l_Lean_Meta_Simp_Context_parent_x3f___default();
lean_mark_persistent(l_Lean_Meta_Simp_Context_parent_x3f___default);
l_Lean_Meta_Simp_State_cache___default___closed__1 = _init_l_Lean_Meta_Simp_State_cache___default___closed__1();

4
stage0/stdlib/Lean/Parser/Term.c generated
View file

@ -2128,7 +2128,6 @@ lean_object* l_Lean_Parser_Term_ellipsis___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_dynamicQuot___elambda__1___closed__8;
lean_object* l_Lean_Parser_Term_borrowed_formatter___closed__2;
lean_object* l_Lean_Parser_Term_arrayRef___elambda__1___closed__1;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__20;
lean_object* l_Lean_Parser_Term_matchAltsWhereDecls_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Tactic_tacticSeqBracketed___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_matchAltsWhereDecls___elambda__1___closed__2;
@ -2819,6 +2818,7 @@ lean_object* l_Lean_Parser_Term_fun___closed__5;
lean_object* l_Lean_Parser_Command_docComment;
lean_object* l_Lean_Parser_Term_matchAltsWhereDecls_formatter___closed__4;
lean_object* l_Lean_Parser_orelseFnCore(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__20;
lean_object* l_Lean_Parser_Term_explicitUniv___closed__2;
lean_object* l___regBuiltin_Lean_Parser_Term_explicitUniv_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_attrInstance___elambda__1___closed__4;
@ -35953,7 +35953,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_myMacro____x40_Init_Notation___hyg_2191____closed__2;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__20;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__20;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}

4
stage0/stdlib/Lean/PrettyPrinter/Delaborator/Basic.c generated
View file

@ -210,7 +210,6 @@ lean_object* l_Lean_initFn____x40_Lean_PrettyPrinter_Delaborator_Basic___hyg_210
uint8_t l_Lean_getPPStructureInstances(lean_object*);
lean_object* l_Lean_initFn____x40_Lean_PrettyPrinter_Delaborator_Basic___hyg_152____closed__4;
lean_object* l_Lean_PrettyPrinter_Delaborator_getExprKind___closed__10;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__20;
lean_object* l_Lean_PrettyPrinter_Delaborator_getUnusedName_bodyUsesSuggestion_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_annotatePos(lean_object*, lean_object*);
lean_object* l_Lean_pp_full__names;
@ -276,6 +275,7 @@ lean_object* lean_panic_fn(lean_object*, lean_object*);
extern lean_object* l_Lean_getSanitizeNames___closed__1;
lean_object* l_Lean_PrettyPrinter_Delaborator_withBindingBody___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_annotatePos_match__2(lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__20;
lean_object* l_Lean_getPPAll___boxed(lean_object*);
lean_object* l_Lean_getPPSafeShadowing___boxed(lean_object*);
lean_object* l_Std_PersistentHashMap_findAtAux___at_Lean_PrettyPrinter_Delaborator_delabFor___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -2968,7 +2968,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5923____closed__20;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5938____closed__20;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}

510
stage0/stdlib/Lean/PrettyPrinter/Delaborator/Builtins.c generated
View file

@ -545,7 +545,6 @@ lean_object* l_Lean_Meta_getMatcherInfo_x3f(lean_object*, lean_object*, lean_obj
lean_object* l___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_unresolveQualifiedName___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldrMUnsafe_fold___at_Lean_PrettyPrinter_Delaborator_delabForall___spec__3___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* l_Lean_PrettyPrinter_Delaborator_delabBVar___closed__1;
lean_object* l_Lean_PrettyPrinter_Delaborator_delabDoElems_delabAndRet(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_delabProj___closed__1;
lean_object* l_Std_PersistentHashMap_find_x3f___at_Lean_PrettyPrinter_Delaborator_delabAppWithUnexpander___spec__2___boxed(lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_delabMVar___closed__1;
@ -23610,91 +23609,6 @@ x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Delaborator_delabDoElems_m
return x_2;
}
}
lean_object* l_Lean_PrettyPrinter_Delaborator_delabDoElems_delabAndRet(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7;
lean_inc(x_5);
lean_inc(x_4);
x_7 = l_Lean_PrettyPrinter_Delaborator_delab(x_1, x_2, x_3, x_4, x_5, x_6);
if (lean_obj_tag(x_7) == 0)
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11;
x_8 = lean_ctor_get(x_7, 0);
lean_inc(x_8);
x_9 = lean_ctor_get(x_7, 1);
lean_inc(x_9);
lean_dec(x_7);
x_10 = l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_PrettyPrinter_Delaborator_delabConst___spec__1___rarg(x_4, x_5, x_9);
lean_dec(x_5);
lean_dec(x_4);
x_11 = !lean_is_exclusive(x_10);
if (x_11 == 0)
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18;
x_12 = lean_ctor_get(x_10, 0);
lean_dec(x_12);
x_13 = l_Array_empty___closed__1;
x_14 = lean_array_push(x_13, x_8);
x_15 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_826____closed__13;
x_16 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_16, 0, x_15);
lean_ctor_set(x_16, 1, x_14);
x_17 = lean_box(0);
x_18 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_18, 0, x_16);
lean_ctor_set(x_18, 1, x_17);
lean_ctor_set(x_10, 0, x_18);
return x_10;
}
else
{
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_19 = lean_ctor_get(x_10, 1);
lean_inc(x_19);
lean_dec(x_10);
x_20 = l_Array_empty___closed__1;
x_21 = lean_array_push(x_20, x_8);
x_22 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_826____closed__13;
x_23 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_23, 0, x_22);
lean_ctor_set(x_23, 1, x_21);
x_24 = lean_box(0);
x_25 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_25, 0, x_23);
lean_ctor_set(x_25, 1, x_24);
x_26 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_26, 0, x_25);
lean_ctor_set(x_26, 1, x_19);
return x_26;
}
}
else
{
uint8_t x_27;
lean_dec(x_5);
lean_dec(x_4);
x_27 = !lean_is_exclusive(x_7);
if (x_27 == 0)
{
return x_7;
}
else
{
lean_object* x_28; lean_object* x_29; lean_object* x_30;
x_28 = lean_ctor_get(x_7, 0);
x_29 = lean_ctor_get(x_7, 1);
lean_inc(x_29);
lean_inc(x_28);
lean_dec(x_7);
x_30 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_30, 0, x_28);
lean_ctor_set(x_30, 1, x_29);
return x_30;
}
}
}
}
lean_object* l_Lean_PrettyPrinter_Delaborator_delabDoElems_prependAndRec(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:
{
@ -24050,9 +23964,14 @@ return x_11;
else
{
lean_object* x_12;
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_12 = l_Lean_PrettyPrinter_Delaborator_delabDoElems_delabAndRet(x_3, x_4, x_5, x_6, x_7, x_8);
x_12 = l_Lean_PrettyPrinter_Delaborator_failure___rarg(x_8);
return x_12;
}
}
@ -24099,214 +24018,291 @@ lean_dec(x_8);
if (x_13 == 0)
{
lean_object* x_14;
x_14 = l_Lean_PrettyPrinter_Delaborator_delabDoElems_delabAndRet(x_1, x_2, x_3, x_4, x_5, x_9);
lean_inc(x_5);
lean_inc(x_4);
x_14 = l_Lean_PrettyPrinter_Delaborator_delab(x_1, x_2, x_3, x_4, x_5, x_9);
if (lean_obj_tag(x_14) == 0)
{
lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18;
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
x_16 = lean_ctor_get(x_14, 1);
lean_inc(x_16);
lean_dec(x_14);
x_17 = l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_PrettyPrinter_Delaborator_delabConst___spec__1___rarg(x_4, x_5, x_16);
lean_dec(x_5);
lean_dec(x_4);
x_18 = !lean_is_exclusive(x_17);
if (x_18 == 0)
{
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;
x_19 = lean_ctor_get(x_17, 0);
lean_dec(x_19);
x_20 = l_Array_empty___closed__1;
x_21 = lean_array_push(x_20, x_15);
x_22 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_826____closed__13;
x_23 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_23, 0, x_22);
lean_ctor_set(x_23, 1, x_21);
x_24 = lean_box(0);
x_25 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_25, 0, x_23);
lean_ctor_set(x_25, 1, x_24);
lean_ctor_set(x_17, 0, x_25);
return x_17;
}
else
{
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;
x_26 = lean_ctor_get(x_17, 1);
lean_inc(x_26);
lean_dec(x_17);
x_27 = l_Array_empty___closed__1;
x_28 = lean_array_push(x_27, x_15);
x_29 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_826____closed__13;
x_30 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_30, 0, x_29);
lean_ctor_set(x_30, 1, x_28);
x_31 = lean_box(0);
x_32 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_32, 0, x_30);
lean_ctor_set(x_32, 1, x_31);
x_33 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_33, 0, x_32);
lean_ctor_set(x_33, 1, x_26);
return x_33;
}
}
else
{
uint8_t x_34;
lean_dec(x_5);
lean_dec(x_4);
x_34 = !lean_is_exclusive(x_14);
if (x_34 == 0)
{
return x_14;
}
else
{
lean_object* x_15; lean_object* x_16;
x_15 = l_Lean_PrettyPrinter_Delaborator_getExpr(x_1, x_2, x_3, x_4, x_5, x_9);
x_16 = lean_ctor_get(x_15, 0);
lean_inc(x_16);
if (lean_obj_tag(x_16) == 8)
{
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; lean_object* x_27;
x_17 = lean_ctor_get(x_15, 1);
lean_inc(x_17);
lean_dec(x_15);
x_18 = lean_ctor_get(x_16, 0);
lean_inc(x_18);
x_19 = lean_ctor_get(x_16, 1);
lean_inc(x_19);
x_20 = lean_ctor_get(x_16, 2);
lean_inc(x_20);
x_21 = lean_ctor_get(x_16, 3);
lean_inc(x_21);
lean_dec(x_16);
lean_inc(x_2);
lean_inc(x_1);
lean_inc(x_21);
x_22 = l_Lean_PrettyPrinter_Delaborator_getUnusedName(x_18, x_21, x_1, x_2, x_3, x_4, x_5, x_17);
x_23 = lean_ctor_get(x_22, 0);
lean_inc(x_23);
x_24 = lean_ctor_get(x_22, 1);
lean_inc(x_24);
lean_dec(x_22);
x_25 = lean_unsigned_to_nat(0u);
x_26 = l_Lean_PrettyPrinter_Delaborator_delabMData___closed__3;
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
lean_inc(x_1);
lean_inc(x_19);
x_27 = l_Lean_PrettyPrinter_Delaborator_descend___rarg(x_19, x_25, x_26, x_1, x_2, x_3, x_4, x_5, x_24);
if (lean_obj_tag(x_27) == 0)
{
lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31;
x_28 = lean_ctor_get(x_27, 0);
lean_inc(x_28);
x_29 = lean_ctor_get(x_27, 1);
lean_inc(x_29);
lean_dec(x_27);
x_30 = lean_unsigned_to_nat(1u);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
lean_inc(x_1);
lean_inc(x_20);
x_31 = l_Lean_PrettyPrinter_Delaborator_descend___rarg(x_20, x_30, x_26, x_1, x_2, x_3, x_4, x_5, x_29);
if (lean_obj_tag(x_31) == 0)
{
lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35;
x_32 = lean_ctor_get(x_31, 0);
lean_inc(x_32);
x_33 = lean_ctor_get(x_31, 1);
lean_inc(x_33);
lean_dec(x_31);
lean_inc(x_23);
x_34 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Delaborator_delabDoElems___lambda__2___boxed), 11, 4);
lean_closure_set(x_34, 0, x_21);
lean_closure_set(x_34, 1, x_23);
lean_closure_set(x_34, 2, x_28);
lean_closure_set(x_34, 3, x_32);
x_35 = l_Lean_Meta_withLetDecl___at_Lean_PrettyPrinter_Delaborator_delabDoElems___spec__1___rarg(x_23, x_19, x_20, x_34, x_1, x_2, x_3, x_4, x_5, x_33);
return x_35;
}
else
{
uint8_t x_36;
lean_dec(x_28);
lean_dec(x_23);
lean_dec(x_21);
lean_dec(x_20);
lean_dec(x_19);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_36 = !lean_is_exclusive(x_31);
if (x_36 == 0)
{
return x_31;
}
else
{
lean_object* x_37; lean_object* x_38; lean_object* x_39;
x_37 = lean_ctor_get(x_31, 0);
x_38 = lean_ctor_get(x_31, 1);
lean_inc(x_38);
lean_inc(x_37);
lean_dec(x_31);
x_39 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_39, 0, x_37);
lean_ctor_set(x_39, 1, x_38);
return x_39;
lean_object* x_35; lean_object* x_36; lean_object* x_37;
x_35 = lean_ctor_get(x_14, 0);
x_36 = lean_ctor_get(x_14, 1);
lean_inc(x_36);
lean_inc(x_35);
lean_dec(x_14);
x_37 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_37, 0, x_35);
lean_ctor_set(x_37, 1, x_36);
return x_37;
}
}
}
else
{
uint8_t x_40;
lean_dec(x_23);
lean_dec(x_21);
lean_dec(x_20);
lean_dec(x_19);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_40 = !lean_is_exclusive(x_27);
if (x_40 == 0)
lean_object* x_38; lean_object* x_39;
x_38 = l_Lean_PrettyPrinter_Delaborator_getExpr(x_1, x_2, x_3, x_4, x_5, x_9);
x_39 = lean_ctor_get(x_38, 0);
lean_inc(x_39);
if (lean_obj_tag(x_39) == 8)
{
return x_27;
}
else
{
lean_object* x_41; lean_object* x_42; lean_object* x_43;
x_41 = lean_ctor_get(x_27, 0);
x_42 = lean_ctor_get(x_27, 1);
lean_inc(x_42);
lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50;
x_40 = lean_ctor_get(x_38, 1);
lean_inc(x_40);
lean_dec(x_38);
x_41 = lean_ctor_get(x_39, 0);
lean_inc(x_41);
lean_dec(x_27);
x_43 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_43, 0, x_41);
lean_ctor_set(x_43, 1, x_42);
return x_43;
}
}
}
else
{
lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48;
lean_dec(x_16);
x_44 = lean_ctor_get(x_15, 1);
x_42 = lean_ctor_get(x_39, 1);
lean_inc(x_42);
x_43 = lean_ctor_get(x_39, 2);
lean_inc(x_43);
x_44 = lean_ctor_get(x_39, 3);
lean_inc(x_44);
lean_dec(x_15);
x_45 = l_Lean_PrettyPrinter_Delaborator_withAppFn___rarg___closed__1;
x_46 = l_Lean_PrettyPrinter_Delaborator_delabDoElems___closed__2;
x_47 = lean_panic_fn(x_45, x_46);
x_48 = lean_apply_6(x_47, x_1, x_2, x_3, x_4, x_5, x_44);
return x_48;
}
}
}
else
{
lean_object* x_49; lean_object* x_50;
lean_dec(x_8);
x_49 = l_Lean_PrettyPrinter_Delaborator_delabTuple___lambda__1___closed__1;
lean_dec(x_39);
lean_inc(x_2);
lean_inc(x_1);
lean_inc(x_44);
x_45 = l_Lean_PrettyPrinter_Delaborator_getUnusedName(x_41, x_44, x_1, x_2, x_3, x_4, x_5, x_40);
x_46 = lean_ctor_get(x_45, 0);
lean_inc(x_46);
x_47 = lean_ctor_get(x_45, 1);
lean_inc(x_47);
lean_dec(x_45);
x_48 = lean_unsigned_to_nat(0u);
x_49 = l_Lean_PrettyPrinter_Delaborator_delabMData___closed__3;
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
lean_inc(x_1);
x_50 = l_Lean_PrettyPrinter_Delaborator_withAppFn___rarg(x_49, x_1, x_2, x_3, x_4, x_5, x_9);
lean_inc(x_42);
x_50 = l_Lean_PrettyPrinter_Delaborator_descend___rarg(x_42, x_48, x_49, x_1, x_2, x_3, x_4, x_5, x_47);
if (lean_obj_tag(x_50) == 0)
{
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_51; lean_object* x_52; lean_object* x_53; lean_object* x_54;
x_51 = lean_ctor_get(x_50, 0);
lean_inc(x_51);
x_52 = lean_ctor_get(x_50, 1);
lean_inc(x_52);
lean_dec(x_50);
x_53 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Delaborator_delabDoElems___lambda__6), 8, 1);
lean_closure_set(x_53, 0, x_51);
x_54 = l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___closed__1;
x_55 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_PrettyPrinter_Delaborator_delabAppExplicit___spec__1___rarg), 8, 2);
lean_closure_set(x_55, 0, x_54);
lean_closure_set(x_55, 1, x_53);
x_56 = l_Lean_PrettyPrinter_Delaborator_withAppArg___rarg(x_55, x_1, x_2, x_3, x_4, x_5, x_52);
return x_56;
x_53 = lean_unsigned_to_nat(1u);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
lean_inc(x_1);
lean_inc(x_43);
x_54 = l_Lean_PrettyPrinter_Delaborator_descend___rarg(x_43, x_53, x_49, x_1, x_2, x_3, x_4, x_5, x_52);
if (lean_obj_tag(x_54) == 0)
{
lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58;
x_55 = lean_ctor_get(x_54, 0);
lean_inc(x_55);
x_56 = lean_ctor_get(x_54, 1);
lean_inc(x_56);
lean_dec(x_54);
lean_inc(x_46);
x_57 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Delaborator_delabDoElems___lambda__2___boxed), 11, 4);
lean_closure_set(x_57, 0, x_44);
lean_closure_set(x_57, 1, x_46);
lean_closure_set(x_57, 2, x_51);
lean_closure_set(x_57, 3, x_55);
x_58 = l_Lean_Meta_withLetDecl___at_Lean_PrettyPrinter_Delaborator_delabDoElems___spec__1___rarg(x_46, x_42, x_43, x_57, x_1, x_2, x_3, x_4, x_5, x_56);
return x_58;
}
else
{
uint8_t x_57;
uint8_t x_59;
lean_dec(x_51);
lean_dec(x_46);
lean_dec(x_44);
lean_dec(x_43);
lean_dec(x_42);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_57 = !lean_is_exclusive(x_50);
if (x_57 == 0)
x_59 = !lean_is_exclusive(x_54);
if (x_59 == 0)
{
return x_54;
}
else
{
lean_object* x_60; lean_object* x_61; lean_object* x_62;
x_60 = lean_ctor_get(x_54, 0);
x_61 = lean_ctor_get(x_54, 1);
lean_inc(x_61);
lean_inc(x_60);
lean_dec(x_54);
x_62 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_62, 0, x_60);
lean_ctor_set(x_62, 1, x_61);
return x_62;
}
}
}
else
{
uint8_t x_63;
lean_dec(x_46);
lean_dec(x_44);
lean_dec(x_43);
lean_dec(x_42);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_63 = !lean_is_exclusive(x_50);
if (x_63 == 0)
{
return x_50;
}
else
{
lean_object* x_58; lean_object* x_59; lean_object* x_60;
x_58 = lean_ctor_get(x_50, 0);
x_59 = lean_ctor_get(x_50, 1);
lean_inc(x_59);
lean_inc(x_58);
lean_object* x_64; lean_object* x_65; lean_object* x_66;
x_64 = lean_ctor_get(x_50, 0);
x_65 = lean_ctor_get(x_50, 1);
lean_inc(x_65);
lean_inc(x_64);
lean_dec(x_50);
x_60 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_60, 0, x_58);
lean_ctor_set(x_60, 1, x_59);
return x_60;
x_66 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_66, 0, x_64);
lean_ctor_set(x_66, 1, x_65);
return x_66;
}
}
}
else
{
lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71;
lean_dec(x_39);
x_67 = lean_ctor_get(x_38, 1);
lean_inc(x_67);
lean_dec(x_38);
x_68 = l_Lean_PrettyPrinter_Delaborator_withAppFn___rarg___closed__1;
x_69 = l_Lean_PrettyPrinter_Delaborator_delabDoElems___closed__2;
x_70 = lean_panic_fn(x_68, x_69);
x_71 = lean_apply_6(x_70, x_1, x_2, x_3, x_4, x_5, x_67);
return x_71;
}
}
}
else
{
lean_object* x_72; lean_object* x_73;
lean_dec(x_8);
x_72 = l_Lean_PrettyPrinter_Delaborator_delabTuple___lambda__1___closed__1;
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
lean_inc(x_1);
x_73 = l_Lean_PrettyPrinter_Delaborator_withAppFn___rarg(x_72, x_1, x_2, x_3, x_4, x_5, x_9);
if (lean_obj_tag(x_73) == 0)
{
lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79;
x_74 = lean_ctor_get(x_73, 0);
lean_inc(x_74);
x_75 = lean_ctor_get(x_73, 1);
lean_inc(x_75);
lean_dec(x_73);
x_76 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Delaborator_delabDoElems___lambda__6), 8, 1);
lean_closure_set(x_76, 0, x_74);
x_77 = l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___closed__1;
x_78 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_PrettyPrinter_Delaborator_delabAppExplicit___spec__1___rarg), 8, 2);
lean_closure_set(x_78, 0, x_77);
lean_closure_set(x_78, 1, x_76);
x_79 = l_Lean_PrettyPrinter_Delaborator_withAppArg___rarg(x_78, x_1, x_2, x_3, x_4, x_5, x_75);
return x_79;
}
else
{
uint8_t x_80;
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_80 = !lean_is_exclusive(x_73);
if (x_80 == 0)
{
return x_73;
}
else
{
lean_object* x_81; lean_object* x_82; lean_object* x_83;
x_81 = lean_ctor_get(x_73, 0);
x_82 = lean_ctor_get(x_73, 1);
lean_inc(x_82);
lean_inc(x_81);
lean_dec(x_73);
x_83 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_83, 0, x_81);
lean_ctor_set(x_83, 1, x_82);
return x_83;
}
}
}

47
stage0/stdlib/Lean/Util/Recognizers.c generated
View file

@ -16,6 +16,7 @@ extern "C" {
lean_object* l_List_reverse___rarg(lean_object*);
lean_object* l_Lean_Expr_iff_x3f(lean_object*);
lean_object* l_Lean_Expr_eq_x3f___boxed(lean_object*);
extern lean_object* l_myMacro____x40_Init_Core___hyg_1796____closed__4;
lean_object* l___private_Lean_Util_Recognizers_0__Lean_Expr_getConstructorVal_x3f_match__1(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3596____closed__5;
@ -39,6 +40,7 @@ lean_object* l___private_Lean_Expr_0__Lean_Expr_getAppArgsAux(lean_object*, lean
lean_object* l_Lean_Expr_const_x3f___boxed(lean_object*);
lean_object* l_Lean_Expr_isConstructorApp_x3f___closed__4;
uint8_t l_Lean_Expr_isHEq(lean_object*);
lean_object* l_Lean_Expr_ne_x3f___boxed(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_Expr_natAdd_x3f___closed__1;
lean_object* l_Lean_Expr_listLit_x3f(lean_object*);
@ -64,6 +66,7 @@ lean_object* l_Lean_Expr_const_x3f_match__1(lean_object*);
lean_object* l_Lean_Expr_constructorApp_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_myMacro____x40_Init_Notation___hyg_14642____closed__5;
lean_object* l___private_Lean_Util_Recognizers_0__Lean_Expr_getConstructorVal_x3f(lean_object*, lean_object*);
lean_object* l_Lean_Expr_ne_x3f(lean_object*);
lean_object* l_Lean_Expr_app3_x3f(lean_object*, lean_object*);
lean_object* l_Lean_Expr_heq_x3f___boxed(lean_object*);
lean_object* l_Lean_Expr_const_x3f(lean_object*);
@ -379,6 +382,50 @@ lean_dec(x_1);
return x_2;
}
}
lean_object* l_Lean_Expr_ne_x3f(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4;
x_2 = l_myMacro____x40_Init_Core___hyg_1796____closed__4;
x_3 = lean_unsigned_to_nat(3u);
x_4 = l_Lean_Expr_isAppOfArity(x_1, x_2, x_3);
if (x_4 == 0)
{
lean_object* x_5;
x_5 = lean_box(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;
x_6 = l_Lean_Expr_appFn_x21(x_1);
x_7 = l_Lean_Expr_appFn_x21(x_6);
x_8 = l_Lean_Expr_appArg_x21(x_7);
lean_dec(x_7);
x_9 = l_Lean_Expr_appArg_x21(x_6);
lean_dec(x_6);
x_10 = l_Lean_Expr_appArg_x21(x_1);
x_11 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_11, 0, x_9);
lean_ctor_set(x_11, 1, x_10);
x_12 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_12, 0, x_8);
lean_ctor_set(x_12, 1, x_11);
x_13 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_13, 0, x_12);
return x_13;
}
}
}
lean_object* l_Lean_Expr_ne_x3f___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Expr_ne_x3f(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* l_Lean_Expr_iff_x3f(lean_object* x_1) {
_start:
{