chore: update stage0
This commit is contained in:
Leonardo de Moura
parent
8525584a78
commit
4e580e78bc
20 changed files with 4890 additions and 2856 deletions
|
|
@ -192,21 +192,20 @@ iterateM₂Aux a₁ a₂ f 0 b
|
|||
@[inline] def foldlM₂ (f : β → α → σ → m β) (b : β) (a₁ : Array α) (a₂ : Array σ): m β :=
|
||||
iterateM₂ a₁ a₂ b (fun _ a₁ a₂ b => f b a₁ a₂)
|
||||
|
||||
-- TODO(Leo): justify termination using wf-rec
|
||||
@[specialize] partial def findMAux (a : Array α) (f : α → m (Option β)) : Nat → m (Option β)
|
||||
@[specialize] partial def findSomeMAux (a : Array α) (f : α → m (Option β)) : Nat → m (Option β)
|
||||
| i =>
|
||||
if h : i < a.size then
|
||||
let idx : Fin a.size := ⟨i, h⟩;
|
||||
do r ← f (a.get idx);
|
||||
match r with
|
||||
| some v => pure r
|
||||
| none => findMAux (i+1)
|
||||
| none => findSomeMAux (i+1)
|
||||
else pure none
|
||||
|
||||
@[inline] def findM? (a : Array α) (f : α → m (Option β)) : m (Option β) :=
|
||||
findMAux a f 0
|
||||
@[inline] def findSomeM? (a : Array α) (f : α → m (Option β)) : m (Option β) :=
|
||||
findSomeMAux a f 0
|
||||
|
||||
@[specialize] partial def findRevMAux (a : Array α) (f : α → m (Option β)) : ∀ (idx : Nat), idx ≤ a.size → m (Option β)
|
||||
@[specialize] partial def findSomeRevMAux (a : Array α) (f : α → m (Option β)) : ∀ (idx : Nat), idx ≤ a.size → m (Option β)
|
||||
| i, h =>
|
||||
if hLt : 0 < i then
|
||||
have i - 1 < i from Nat.subLt hLt (Nat.zeroLtSucc 0);
|
||||
|
|
@ -218,14 +217,46 @@ findMAux a f 0
|
|||
| some v => pure r
|
||||
| none =>
|
||||
have i - 1 ≤ a.size from Nat.leOfLt this;
|
||||
findRevMAux (i-1) this
|
||||
findSomeRevMAux (i-1) this
|
||||
else pure none
|
||||
|
||||
@[inline] def findRevM? (a : Array α) (f : α → m (Option β)) : m (Option β) :=
|
||||
findRevMAux a f a.size (Nat.leRefl _)
|
||||
|
||||
@[inline] def findSomeRevM? (a : Array α) (f : α → m (Option β)) : m (Option β) :=
|
||||
findSomeRevMAux a f a.size (Nat.leRefl _)
|
||||
end
|
||||
|
||||
-- TODO(Leo): justify termination using wf-rec
|
||||
@[specialize] partial def findMAux {α : Type} {m : Type → Type} [Monad m] (a : Array α) (p : α → m Bool) : Nat → m (Option α)
|
||||
| i =>
|
||||
if h : i < a.size then do
|
||||
let v := a.get ⟨i, h⟩;
|
||||
condM (p v) (pure (some v)) (findMAux (i+1))
|
||||
else pure none
|
||||
|
||||
@[inline] def findM? {α : Type} {m : Type → Type} [Monad m] (a : Array α) (p : α → m Bool) : m (Option α) :=
|
||||
findMAux a p 0
|
||||
|
||||
@[inline] def find? {α : Type} (a : Array α) (p : α → Bool) : Option α :=
|
||||
Id.run $ a.findM? p
|
||||
|
||||
@[specialize] partial def findRevMAux {α : Type} {m : Type → Type} [Monad m] (a : Array α) (p : α → m Bool) : ∀ (idx : Nat), idx ≤ a.size → m (Option α)
|
||||
| i, h =>
|
||||
if hLt : 0 < i then
|
||||
have i - 1 < i from Nat.subLt hLt (Nat.zeroLtSucc 0);
|
||||
have i - 1 < a.size from Nat.ltOfLtOfLe this h;
|
||||
let v := a.get ⟨i - 1, this⟩;
|
||||
do {
|
||||
condM (p v) (pure (some v)) $
|
||||
have i - 1 ≤ a.size from Nat.leOfLt this;
|
||||
findRevMAux (i-1) this
|
||||
}
|
||||
else pure none
|
||||
|
||||
@[inline] def findRevM? {α : Type} {m : Type → Type} [Monad m] (a : Array α) (p : α → m Bool) : m (Option α) :=
|
||||
findRevMAux a p a.size (Nat.leRefl _)
|
||||
|
||||
@[inline] def findRev? {α : Type} (a : Array α) (p : α → Bool) : Option α :=
|
||||
Id.run $ a.findRevM? p
|
||||
|
||||
section
|
||||
variables {β : Type w} {σ : Type u}
|
||||
|
||||
|
|
@ -247,19 +278,19 @@ Id.run $ iterateM₂Aux a₁ a₂ f 0 b
|
|||
@[inline] def foldl₂ (f : β → α → σ → β) (b : β) (a₁ : Array α) (a₂ : Array σ) : β :=
|
||||
iterate₂ a₁ a₂ b (fun _ a₁ a₂ b => f b a₁ a₂)
|
||||
|
||||
@[inline] def find? (a : Array α) (f : α → Option β) : Option β :=
|
||||
Id.run $ findMAux a f 0
|
||||
@[inline] def findSome? (a : Array α) (f : α → Option β) : Option β :=
|
||||
Id.run $ findSomeMAux a f 0
|
||||
|
||||
@[inline] def find! [Inhabited β] (a : Array α) (f : α → Option β) : β :=
|
||||
match find? a f with
|
||||
@[inline] def findSome! [Inhabited β] (a : Array α) (f : α → Option β) : β :=
|
||||
match findSome? a f with
|
||||
| some b => b
|
||||
| none => panic! "failed to find element"
|
||||
|
||||
@[inline] def findRev? (a : Array α) (f : α → Option β) : Option β :=
|
||||
Id.run $ findRevMAux a f a.size (Nat.leRefl _)
|
||||
@[inline] def findSomeRev? (a : Array α) (f : α → Option β) : Option β :=
|
||||
Id.run $ findSomeRevMAux a f a.size (Nat.leRefl _)
|
||||
|
||||
@[inline] def findRev! [Inhabited β] (a : Array α) (f : α → Option β) : β :=
|
||||
match findRev? a f with
|
||||
@[inline] def findSomeRev! [Inhabited β] (a : Array α) (f : α → Option β) : β :=
|
||||
match findSomeRev? a f with
|
||||
| some b => b
|
||||
| none => panic! "failed to find element"
|
||||
|
||||
|
|
|
|||
|
|
@ -197,24 +197,24 @@ variable {β : Type v}
|
|||
@[specialize] def foldlM (t : PersistentArray α) (f : β → α → m β) (b : β) : m β := do
|
||||
b ← foldlMAux f t.root b; t.tail.foldlM f b
|
||||
|
||||
@[specialize] partial def findMAux (f : α → m (Option β)) : PersistentArrayNode α → m (Option β)
|
||||
| node cs => cs.findM? (fun c => findMAux c)
|
||||
| leaf vs => vs.findM? f
|
||||
@[specialize] partial def findSomeMAux (f : α → m (Option β)) : PersistentArrayNode α → m (Option β)
|
||||
| node cs => cs.findSomeM? (fun c => findSomeMAux c)
|
||||
| leaf vs => vs.findSomeM? f
|
||||
|
||||
@[specialize] def findM? (t : PersistentArray α) (f : α → m (Option β)) : m (Option β) := do
|
||||
b ← findMAux f t.root;
|
||||
@[specialize] def findSomeM? (t : PersistentArray α) (f : α → m (Option β)) : m (Option β) := do
|
||||
b ← findSomeMAux f t.root;
|
||||
match b with
|
||||
| none => t.tail.findM? f
|
||||
| none => t.tail.findSomeM? f
|
||||
| some b => pure (some b)
|
||||
|
||||
@[specialize] partial def findRevMAux (f : α → m (Option β)) : PersistentArrayNode α → m (Option β)
|
||||
| node cs => cs.findRevM? (fun c => findRevMAux c)
|
||||
| leaf vs => vs.findRevM? f
|
||||
@[specialize] partial def findSomeRevMAux (f : α → m (Option β)) : PersistentArrayNode α → m (Option β)
|
||||
| node cs => cs.findSomeRevM? (fun c => findSomeRevMAux c)
|
||||
| leaf vs => vs.findSomeRevM? f
|
||||
|
||||
@[specialize] def findRevM? (t : PersistentArray α) (f : α → m (Option β)) : m (Option β) := do
|
||||
b ← t.tail.findRevM? f;
|
||||
@[specialize] def findSomeRevM? (t : PersistentArray α) (f : α → m (Option β)) : m (Option β) := do
|
||||
b ← t.tail.findSomeRevM? f;
|
||||
match b with
|
||||
| none => findRevMAux f t.root
|
||||
| none => findSomeRevMAux f t.root
|
||||
| some b => pure (some b)
|
||||
|
||||
partial def foldlFromMAux (f : β → α → m β) : PersistentArrayNode α → USize → USize → β → m β
|
||||
|
|
@ -252,11 +252,11 @@ else t₂.foldl PersistentArray.push t₁
|
|||
|
||||
instance : HasAppend (PersistentArray α) := ⟨append⟩
|
||||
|
||||
@[inline] def find? {β} (t : PersistentArray α) (f : α → (Option β)) : Option β :=
|
||||
Id.run (t.findM? f)
|
||||
@[inline] def findSome? {β} (t : PersistentArray α) (f : α → (Option β)) : Option β :=
|
||||
Id.run (t.findSomeM? f)
|
||||
|
||||
@[inline] def findRev? {β} (t : PersistentArray α) (f : α → (Option β)) : Option β :=
|
||||
Id.run (t.findRevM? f)
|
||||
@[inline] def findSomeRev? {β} (t : PersistentArray α) (f : α → (Option β)) : Option β :=
|
||||
Id.run (t.findSomeRevM? f)
|
||||
|
||||
@[inline] def foldlFrom {β} (t : PersistentArray α) (f : β → α → β) (b : β) (ini : Nat) : β :=
|
||||
Id.run (t.foldlFromM f b ini)
|
||||
|
|
|
|||
|
|
@ -124,7 +124,7 @@ def addDecls (decls : Array Decl) : CompilerM Unit :=
|
|||
decls.forM addDecl
|
||||
|
||||
def findEnvDecl' (env : Environment) (n : Name) (decls : Array Decl) : Option Decl :=
|
||||
match decls.find? (fun decl => if decl.name == n then some decl else none) with
|
||||
match decls.find? (fun decl => decl.name == n) with
|
||||
| some decl => some decl
|
||||
| none => (declMapExt.getState env).find? n
|
||||
|
||||
|
|
|
|||
|
|
@ -93,7 +93,7 @@ stx.isOfKind nullKind && stx.getArgs.any isAntiquotSplice
|
|||
explicit kinds behave the same at runtime. So we replace `choice` nodes that contain
|
||||
at least one implicit antiquotation with that antiquotation. -/
|
||||
private partial def elimAntiquotChoices : Syntax → Syntax
|
||||
| Syntax.node `choice args => match args.find? (fun arg => if antiquotKind? arg == Name.anonymous then some arg else none) with
|
||||
| Syntax.node `choice args => match args.find? (fun arg => antiquotKind? arg == Name.anonymous) with
|
||||
| some anti => anti
|
||||
| none => Syntax.node `choice $ args.map elimAntiquotChoices
|
||||
| Syntax.node k args => Syntax.node k $ args.map elimAntiquotChoices
|
||||
|
|
|
|||
|
|
@ -180,26 +180,54 @@ fun stx => do
|
|||
trace `Elab stx $ fun _ => d;
|
||||
withMacroExpansion stx d $ elabCommand d
|
||||
|
||||
def getMacroRulesAltKind (alt : Syntax) : CommandElabM SyntaxNodeKind :=
|
||||
def elabMacroRulesAux (k : SyntaxNodeKind) (alts : Array Syntax) : CommandElabM Syntax := do
|
||||
alts ← alts.mapSepElemsM $ fun alt => do {
|
||||
let lhs := alt.getArg 0;
|
||||
let pat := lhs.getArg 0;
|
||||
match_syntax pat with
|
||||
| `(`($quot)) =>
|
||||
let k' := quot.getKind;
|
||||
if k' == k then
|
||||
pure alt
|
||||
else if k' == choiceKind then do
|
||||
match quot.getArgs.find? $ fun quotAlt => quotAlt.getKind == k with
|
||||
| none => throwError alt ("invalid macro_rules alternative, expected syntax node kind '" ++ k ++ "'")
|
||||
| some quot => do
|
||||
pat ← `(`($quot));
|
||||
let lhs := lhs.setArg 0 pat;
|
||||
pure $ alt.setArg 0 lhs
|
||||
else
|
||||
throwError alt ("invalid macro_rules alternative, unexpected syntax node kind '" ++ k' ++ "'")
|
||||
| stx => throwUnsupportedSyntax
|
||||
};
|
||||
`(@[macro $(Lean.mkIdent k)] def myMacro : Macro := fun stx => match_syntax stx with $alts:matchAlt* | _ => throw Lean.Macro.Exception.unsupportedSyntax)
|
||||
|
||||
def inferMacroRulesAltKind (alt : Syntax) : CommandElabM SyntaxNodeKind :=
|
||||
match_syntax (alt.getArg 0).getArg 0 with
|
||||
| `(`($quot)) => pure quot.getKind
|
||||
| stx => throwUnsupportedSyntax
|
||||
|
||||
def elabMacroRulesAux (alts : Array Syntax) : CommandElabM Syntax := do
|
||||
k ← getMacroRulesAltKind (alts.get! 0);
|
||||
altsK ← alts.filterSepElemsM (fun alt => do k' ← getMacroRulesAltKind alt; pure $ k == k');
|
||||
altsNotK ← alts.filterSepElemsM (fun alt => do k' ← getMacroRulesAltKind alt; pure $ k != k');
|
||||
altsKDef ← `(@[macro $(Lean.mkIdent k)] def myMacro : Macro := fun stx => match_syntax stx with $altsK:matchAlt* | _ => throw Lean.Macro.Exception.unsupportedSyntax);
|
||||
if altsNotK.isEmpty then
|
||||
pure altsKDef
|
||||
else
|
||||
`($altsKDef:command macro_rules $altsNotK:matchAlt*)
|
||||
def elabNoKindMacroRulesAux (alts : Array Syntax) : CommandElabM Syntax := do
|
||||
k ← inferMacroRulesAltKind (alts.get! 0);
|
||||
if k == choiceKind then
|
||||
throwError (alts.get! 0)
|
||||
"invalid macro_rules alternative, multiple interpretations for pattern (solution: specify node kind using `macro_rules [<kind>] ...`)"
|
||||
else do
|
||||
altsK ← alts.filterSepElemsM (fun alt => do k' ← inferMacroRulesAltKind alt; pure $ k == k');
|
||||
altsNotK ← alts.filterSepElemsM (fun alt => do k' ← inferMacroRulesAltKind alt; pure $ k != k');
|
||||
defCmd ← elabMacroRulesAux k altsK;
|
||||
if altsNotK.isEmpty then
|
||||
pure defCmd
|
||||
else
|
||||
`($defCmd:command macro_rules $altsNotK:matchAlt*)
|
||||
|
||||
@[builtinCommandElab «macro_rules»] def elabMacroRules : CommandElab :=
|
||||
adaptExpander $ fun stx => match_syntax stx with
|
||||
| `(macro_rules $alts:matchAlt*) => elabMacroRulesAux alts
|
||||
| `(macro_rules | $alts:matchAlt*) => elabMacroRulesAux alts
|
||||
| _ => throwUnsupportedSyntax
|
||||
| `(macro_rules $alts:matchAlt*) => elabNoKindMacroRulesAux alts
|
||||
| `(macro_rules | $alts:matchAlt*) => elabNoKindMacroRulesAux alts
|
||||
| `(macro_rules [$kind] $alts:matchAlt*) => elabMacroRulesAux kind.getId alts
|
||||
| `(macro_rules [$kind] | $alts:matchAlt*) => elabMacroRulesAux kind.getId alts
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
/- We just ignore Lean3 notation declaration commands. -/
|
||||
@[builtinCommandElab «mixfix»] def elabMixfix : CommandElab := fun _ => pure ()
|
||||
|
|
|
|||
|
|
@ -342,8 +342,10 @@ private partial def elabAppFn (ref : Syntax) : Syntax → List LVal → Array Na
|
|||
us ← if us.isEmpty then pure [] else elabExplicitUniv (us.get! 0);
|
||||
elabAppFnId ref id us lvals namedArgs args expectedType? explicit acc
|
||||
| _ => do
|
||||
f ← elabTerm f none;
|
||||
s ← observing $ elabAppLVals ref f lvals namedArgs args expectedType? explicit;
|
||||
s ← observing $ do {
|
||||
f ← elabTerm f none;
|
||||
elabAppLVals ref f lvals namedArgs args expectedType? explicit
|
||||
};
|
||||
pure $ acc.push s
|
||||
|
||||
private def getSuccess (candidates : Array TermElabResult) : Array TermElabResult :=
|
||||
|
|
|
|||
|
|
@ -141,7 +141,7 @@ match lctx with
|
|||
|
||||
@[export lean_local_ctx_find_from_user_name]
|
||||
def findFromUserName? (lctx : LocalContext) (userName : Name) : Option LocalDecl :=
|
||||
lctx.decls.findRev? (fun decl =>
|
||||
lctx.decls.findSomeRev? (fun decl =>
|
||||
match decl with
|
||||
| none => none
|
||||
| some decl => if decl.userName == userName then some decl else none)
|
||||
|
|
@ -202,12 +202,12 @@ lctx.decls.forM $ fun decl => match decl with
|
|||
| some decl => f decl *> pure PUnit.unit
|
||||
|
||||
@[specialize] def findDeclM? (lctx : LocalContext) (f : LocalDecl → m (Option β)) : m (Option β) :=
|
||||
lctx.decls.findM? $ fun decl => match decl with
|
||||
lctx.decls.findSomeM? $ fun decl => match decl with
|
||||
| none => pure none
|
||||
| some decl => f decl
|
||||
|
||||
@[specialize] def findDeclRevM? (lctx : LocalContext) (f : LocalDecl → m (Option β)) : m (Option β) :=
|
||||
lctx.decls.findRevM? $ fun decl => match decl with
|
||||
lctx.decls.findSomeRevM? $ fun decl => match decl with
|
||||
| none => pure none
|
||||
| some decl => f decl
|
||||
|
||||
|
|
|
|||
|
|
@ -988,7 +988,7 @@ match prev.getTailInfo with
|
|||
| none => false
|
||||
|
||||
private def pickNonNone (stack : Array Syntax) : Syntax :=
|
||||
match stack.findRev? $ fun stx => if stx.isNone then none else some stx with
|
||||
match stack.findRev? $ fun stx => !stx.isNone with
|
||||
| none => Syntax.missing
|
||||
| some stx => stx
|
||||
|
||||
|
|
|
|||
|
|
@ -84,7 +84,7 @@ partial def findField? (env : Environment) : Name → Name → Option Name
|
|||
if (getStructureFields env structName).contains fieldName then
|
||||
some structName
|
||||
else
|
||||
(getParentStructures env structName).find? $ fun parentStructName => findField? parentStructName fieldName
|
||||
(getParentStructures env structName).findSome? $ fun parentStructName => findField? parentStructName fieldName
|
||||
|
||||
private partial def getStructureFieldsFlattenedAux (env : Environment) : Name → Array Name → Array Name
|
||||
| structName, fullNames =>
|
||||
|
|
@ -127,7 +127,7 @@ partial def getPathToBaseStructureAux (env : Environment) (baseStructName : Name
|
|||
some path.reverse
|
||||
else
|
||||
let fieldNames := getStructureFields env structName;
|
||||
fieldNames.find? $ fun fieldName =>
|
||||
fieldNames.findSome? $ fun fieldName =>
|
||||
match isSubobjectField? env structName fieldName with
|
||||
| none => none
|
||||
| some parentStructName => getPathToBaseStructureAux parentStructName ((structName ++ fieldName) :: path)
|
||||
|
|
|
|||
|
|
@ -191,13 +191,13 @@ SourceInfo.pos <$> stx.getHeadInfo
|
|||
partial def getTailWithInfo : Syntax → Option Syntax
|
||||
| stx@(atom (some _) _) => some stx
|
||||
| stx@(ident (some _) _ _ _) => some stx
|
||||
| node _ args => args.findRev? getTailWithInfo
|
||||
| node _ args => args.findSomeRev? getTailWithInfo
|
||||
| _ => none
|
||||
|
||||
partial def getTailInfo : Syntax → Option SourceInfo
|
||||
| atom info _ => info
|
||||
| ident info _ _ _ => info
|
||||
| node _ args => args.findRev? getTailInfo
|
||||
| node _ args => args.findSomeRev? getTailInfo
|
||||
| _ => none
|
||||
|
||||
@[specialize] private partial def updateLast {α} [Inhabited α] (a : Array α) (f : α → Option α) : Nat → Option (Array α)
|
||||
|
|
|
|||
|
|
@ -245,7 +245,7 @@ match stx with
|
|||
partial def getHeadInfo : Syntax → Option SourceInfo
|
||||
| atom info _ => info
|
||||
| ident info _ _ _ => info
|
||||
| node _ args => args.find? getHeadInfo
|
||||
| node _ args => args.findSome? getHeadInfo
|
||||
| _ => none
|
||||
|
||||
end Syntax
|
||||
|
|
@ -782,4 +782,22 @@ filterSepElemsMAux a p 0 #[]
|
|||
def filterSepElems (a : Array Syntax) (p : Syntax → Bool) : Array Syntax :=
|
||||
Id.run $ a.filterSepElemsM p
|
||||
|
||||
private partial def mapSepElemsMAux {m : Type → Type} [Monad m] (a : Array Syntax) (f : Syntax → m Syntax) : Nat → Array Syntax → m (Array Syntax)
|
||||
| i, acc =>
|
||||
if h : i < a.size then do
|
||||
let stx := a.get ⟨i, h⟩;
|
||||
if i % 2 == 0 then do
|
||||
stx ← f stx;
|
||||
mapSepElemsMAux (i+1) (acc.push stx)
|
||||
else
|
||||
mapSepElemsMAux (i+1) (acc.push stx)
|
||||
else
|
||||
pure acc
|
||||
|
||||
def mapSepElemsM {m : Type → Type} [Monad m] (a : Array Syntax) (f : Syntax → m Syntax) : m (Array Syntax) :=
|
||||
mapSepElemsMAux a f 0 #[]
|
||||
|
||||
def mapSepElems (a : Array Syntax) (f : Syntax → Syntax) : Array Syntax :=
|
||||
Id.run $ a.mapSepElemsM f
|
||||
|
||||
end Array
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
File diff suppressed because it is too large
Load diff
File diff suppressed because it is too large
Load diff
File diff suppressed because it is too large
Load diff
|
|
@ -24,8 +24,11 @@ lean_object* l_PersistentArray_anyMAux___main___at_Lean_LocalContext_anyM___spec
|
|||
size_t l_USize_add(size_t, size_t);
|
||||
lean_object* l_Lean_Name_eraseMacroScopes(lean_object*);
|
||||
lean_object* l_Lean_LocalDecl_userName___boxed(lean_object*);
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__6___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_foldlM___at_Lean_LocalContext_foldl___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findSomeRevM_x3f___at_Lean_LocalContext_findFromUserName_x3f___spec__1(lean_object*, lean_object*);
|
||||
lean_object* lean_local_ctx_get_unused_name(lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__5(lean_object*);
|
||||
lean_object* l_Lean_LocalContext_usesUserName___boxed(lean_object*, lean_object*);
|
||||
uint8_t lean_local_ctx_is_empty(lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_mkLocalDecl___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -34,51 +37,47 @@ lean_object* l_Lean_LocalContext_findDeclRev_x3f___rarg___boxed(lean_object*, le
|
|||
uint8_t l_Array_anyRangeMAux___main___at_Lean_LocalContext_any___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_allM___spec__3___boxed(lean_object*);
|
||||
lean_object* l_PersistentHashMap_findAux___main___at_Lean_LocalContext_find_x3f___spec__2(lean_object*, size_t, lean_object*);
|
||||
lean_object* l_PersistentArray_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__4___rarg___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_foldlFrom___spec__6___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_isSubPrefixOfAux___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_LocalContext_1__popTailNoneAux___main(lean_object*);
|
||||
lean_object* l_PersistentArray_anyM___at_Lean_LocalContext_allM___spec__1(lean_object*);
|
||||
lean_object* l_Array_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__4___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_foldlFrom___spec__6___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_insertAux___main___at_Lean_LocalContext_mkLocalDecl___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_anyM___spec__3___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t lean_name_eq(lean_object*, lean_object*);
|
||||
extern size_t l_PersistentHashMap_insertAux___main___rarg___closed__2;
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__3___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_allM___spec__4___boxed(lean_object*);
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_anyM___spec__4(lean_object*);
|
||||
lean_object* l_Lean_LocalContext_foldlFromM___at_Lean_LocalContext_foldlFrom___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findSomeM_x3f___at_Lean_LocalContext_findDecl_x3f___spec__2___rarg(lean_object*, lean_object*);
|
||||
lean_object* lean_local_ctx_mk_let_decl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__3___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_any___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_foldlFrom___spec__10(lean_object*);
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_anyM___spec__4___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
|
||||
lean_object* l_Lean_LocalDecl_value___closed__3;
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__5___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_allM___spec__3___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_anyM___spec__4___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_Inhabited;
|
||||
lean_object* lean_local_ctx_erase(lean_object*, lean_object*);
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__6___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
size_t l_USize_sub(size_t, size_t);
|
||||
lean_object* l___private_Init_Util_1__mkPanicMessage(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_findDeclM_x3f(lean_object*);
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_allM___spec__4___rarg___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__3___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Nat_foldRevAux___main___at_Lean_LocalContext_mkLambda___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_foldlFromM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_foldlFrom___spec__8(lean_object*);
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__4___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_anyM___spec__3___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Array_anyRangeMAux___main___at_Lean_LocalContext_any___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__5(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_get_x21(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalDecl_binderInfo___boxed(lean_object*);
|
||||
uint8_t l_Lean_LocalContext_containsFVar(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_anyMAux___main___at_Lean_LocalContext_allM___spec__2___boxed(lean_object*);
|
||||
lean_object* l_Lean_LocalDecl_index___boxed(lean_object*);
|
||||
lean_object* l_Array_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__6(lean_object*);
|
||||
lean_object* l_Lean_LocalDecl_Inhabited___closed__1;
|
||||
lean_object* lean_local_ctx_find_from_user_name(lean_object*, lean_object*);
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__6(lean_object*);
|
||||
lean_object* l_PersistentHashMap_isUnaryNode___rarg(lean_object*);
|
||||
uint8_t l_Lean_LocalContext_isSubPrefixOfAux(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -96,22 +95,23 @@ lean_object* l_Lean_LocalContext_forM___boxed(lean_object*);
|
|||
lean_object* l_PersistentArray_foldlMAux___main___at_Lean_LocalContext_foldl___spec__3___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_findAtAux___main___at_Lean_LocalContext_find_x3f___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_foldlFrom___spec__9(lean_object*);
|
||||
lean_object* l_PersistentArray_findM_x3f___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
size_t l_USize_shiftRight(size_t, size_t);
|
||||
lean_object* l_Array_indexOfAux___main___at_Lean_LocalContext_erase___spec__3(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__4(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_PersistentArray_anyMAux___main___at_Lean_LocalContext_any___spec__2(lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_LocalContext_2__getUnusedNameAux(lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Lean_LocalContext_contains(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_anyMAux___main___at_Lean_LocalContext_any___spec__2___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_foldl___spec__4___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findSomeM_x3f___at_Lean_LocalContext_findDecl_x3f___spec__2___rarg___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_any___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_Inhabited___closed__1;
|
||||
lean_object* l_Lean_LocalContext_anyM___boxed(lean_object*);
|
||||
lean_object* lean_nat_add(lean_object*, lean_object*);
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findSomeRevM_x3f___at_Lean_LocalContext_findDeclRev_x3f___spec__2___rarg(lean_object*, lean_object*);
|
||||
uint8_t l_Array_anyRangeMAux___main___at_Lean_LocalContext_all___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__4(lean_object*);
|
||||
lean_object* l_PersistentHashMap_erase___at_Lean_LocalContext_erase___spec__1(lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalDecl_value___closed__2;
|
||||
lean_object* l_PersistentHashMap_find_x3f___at_Lean_LocalContext_find_x3f___spec__1(lean_object*, lean_object*);
|
||||
uint8_t lean_expr_has_loose_bvar(lean_object*, lean_object*);
|
||||
|
|
@ -121,6 +121,8 @@ lean_object* l_PersistentHashMap_insertAtCollisionNodeAux___main___at_Lean_Local
|
|||
lean_object* l_Lean_LocalDecl_updateUserName(lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_foldlFrom___spec__8___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_PersistentHashMap_containsAtAux___main___at_Lean_LocalContext_contains___spec__3(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__3___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__6___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_Inhabited___closed__2;
|
||||
lean_object* l_PersistentArray_foldlFromMAux___main___at_Lean_LocalContext_foldlFrom___spec__3(lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_foldlFrom___spec__9___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -133,50 +135,46 @@ lean_object* l_Lean_LocalDecl_value(lean_object*);
|
|||
lean_object* l_Lean_LocalContext_findDeclRevM_x3f___boxed(lean_object*);
|
||||
lean_object* lean_local_ctx_num_indices(lean_object*);
|
||||
lean_object* l_Lean_LocalDecl_isLet___boxed(lean_object*);
|
||||
lean_object* l_PersistentArray_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__3___rarg___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Nat_foldRevAux___main___at_Lean_LocalContext_mkBinding___spec__1(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__4___rarg(lean_object*, lean_object*);
|
||||
lean_object* lean_array_fget(lean_object*, lean_object*);
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__5___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_anyM___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Expr_Inhabited___closed__1;
|
||||
lean_object* l_Lean_LocalDecl_type___boxed(lean_object*);
|
||||
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_mkBinding(uint8_t, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_foldl___spec__6___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_get_x21___at___private_Init_Lean_LocalContext_1__popTailNoneAux___main___spec__1___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__3(lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_foldl___spec__5___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_anyM___spec__5(lean_object*);
|
||||
lean_object* l_Lean_LocalContext_forM(lean_object*);
|
||||
lean_object* lean_nat_sub(lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__4(lean_object*);
|
||||
lean_object* l_PersistentHashMap_contains___at_Lean_LocalContext_contains___spec__1___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_findDecl_x3f(lean_object*);
|
||||
lean_object* l_PersistentArray_anyM___at_Lean_LocalContext_anyM___spec__1___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findRevM_x3f___at_Lean_LocalContext_findDeclRev_x3f___spec__2___rarg___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_foldlFrom___spec__10___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_all___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_PersistentArray_anyM___at_Lean_LocalContext_all___spec__1(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findSomeRevM_x3f___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_mkLocalDecl___spec__4(size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_getAux___main___at___private_Init_Lean_LocalContext_1__popTailNoneAux___main___spec__2___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_foldlM___at_Lean_LocalContext_foldl___spec__1(lean_object*);
|
||||
lean_object* l_PersistentArray_anyM___at_Lean_LocalContext_allM___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__3(lean_object*);
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_anyM___spec__5___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Nat_foldRevAux___main___at_Lean_LocalContext_mkBinding___spec__1___closed__1;
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_any___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Expr_fvarId_x21(lean_object*);
|
||||
lean_object* l_PersistentArray_findM_x3f___at_Lean_LocalContext_findDecl_x3f___spec__2___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_Nat_foldRevAux___main___at_Lean_LocalContext_mkBinding___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__5(lean_object*);
|
||||
uint8_t l_PersistentHashMap_isEmpty___at_Lean_LocalContext_isEmpty___spec__1(lean_object*);
|
||||
lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__5___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_findDeclM_x3f___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_anyM___spec__5___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findM_x3f___at_Lean_LocalContext_findDecl_x3f___spec__2___rarg___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Name_appendIndexAfter(lean_object*, lean_object*);
|
||||
lean_object* l_Array_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__5___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_findDeclRev_x3f___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_Array_indexOfAux___main___at_Lean_LocalContext_erase___spec__3___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_allM___spec__3___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -193,6 +191,7 @@ lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_allM___spec__5__
|
|||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_allM___spec__4___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_foldlFromM___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_PersistentHashMap_insertAux___main___rarg___closed__3;
|
||||
lean_object* l_PersistentArray_findSomeRevM_x3f___at_Lean_LocalContext_findDeclRev_x3f___spec__2___rarg___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_foldlFromM___at_Lean_LocalContext_foldlFrom___spec__1(lean_object*);
|
||||
lean_object* l_Nat_foldRevAux___main___at_Lean_LocalContext_mkLambda___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_anyMAux___main___at_Lean_LocalContext_anyM___spec__2(lean_object*);
|
||||
|
|
@ -212,30 +211,32 @@ size_t l_USize_shiftLeft(size_t, size_t);
|
|||
lean_object* l_Lean_LocalDecl_Inhabited;
|
||||
lean_object* l_PersistentHashMap_containsAux___main___at_Lean_LocalContext_contains___spec__2___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_anyM___spec__4___boxed(lean_object*);
|
||||
lean_object* l_Array_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__5(lean_object*);
|
||||
lean_object* l_Lean_LocalDecl_value___closed__1;
|
||||
lean_object* l_PersistentHashMap_isEmpty___at_Lean_LocalContext_isEmpty___spec__1___boxed(lean_object*);
|
||||
lean_object* l_PersistentArray_getAux___main___at___private_Init_Lean_LocalContext_1__popTailNoneAux___main___spec__2(lean_object*, size_t, size_t);
|
||||
lean_object* l_Lean_LocalContext_foldlM___at_Lean_LocalContext_foldl___spec__1___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findRevM_x3f___at_Lean_LocalContext_findFromUserName_x3f___spec__1(lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_foldlFromM___at_Lean_LocalContext_foldlFrom___spec__1___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_foldl___spec__6(lean_object*);
|
||||
lean_object* l_PersistentArray_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__3___rarg___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__3(lean_object*);
|
||||
lean_object* l_Nat_foldRevAux___main___at_Lean_LocalContext_mkForall___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__6___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__3___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_PersistentHashMap_contains___at_Lean_LocalContext_contains___spec__1(lean_object*, lean_object*);
|
||||
lean_object* lean_local_ctx_pop(lean_object*);
|
||||
lean_object* l_PersistentArray_anyMAux___main___at_Lean_LocalContext_allM___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_isSubPrefixOfAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__5___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalDecl_toExpr(lean_object*);
|
||||
extern lean_object* l_PersistentHashMap_empty___rarg___closed__2;
|
||||
lean_object* l_Lean_mkLambda(lean_object*, uint8_t, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findM_x3f___at_Lean_LocalContext_findDecl_x3f___spec__2(lean_object*);
|
||||
size_t l_USize_mul(size_t, size_t);
|
||||
lean_object* l_Lean_LocalDecl_toExpr___boxed(lean_object*);
|
||||
uint8_t l_Lean_LocalContext_all(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_findFVar_x3f___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_findAtAux___main___at_Lean_LocalContext_find_x3f___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_foldlMAux___main___at_Lean_LocalContext_foldl___spec__3(lean_object*);
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__4___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_foldlFrom___spec__5(lean_object*);
|
||||
lean_object* l_Lean_mkFVar(lean_object*);
|
||||
lean_object* l_Lean_LocalContext_findDeclRevM_x3f___at_Lean_LocalContext_findDeclRev_x3f___spec__1(lean_object*);
|
||||
|
|
@ -246,20 +247,22 @@ lean_object* l_PersistentHashMap_findAux___main___at_Lean_LocalContext_find_x3f_
|
|||
lean_object* l_Lean_LocalContext_findDeclM_x3f___boxed(lean_object*);
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_allM___spec__4___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
|
||||
lean_object* l_PersistentArray_foldlMAux___main___at_Lean_LocalContext_foldlFrom___spec__4___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__5___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
size_t l_USize_land(size_t, size_t);
|
||||
lean_object* l_PersistentArray_anyM___at_Lean_LocalContext_allM___spec__1___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
|
||||
lean_object* l_Lean_LocalDecl_value_x3f___boxed(lean_object*);
|
||||
lean_object* l_Lean_LocalDecl_fvarId(lean_object*);
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_allM___spec__3___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
|
||||
lean_object* l_PersistentArray_findSomeM_x3f___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_foldlM___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_allM___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__5___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Array_anyRangeMAux___main___at_Lean_LocalContext_all___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalDecl_type(lean_object*);
|
||||
lean_object* l_Lean_LocalDecl_value_x3f(lean_object*);
|
||||
lean_object* lean_local_ctx_mk_local_decl(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
|
||||
lean_object* l_Lean_LocalContext_foldlFrom___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_foldlFromMAux___main___at_Lean_LocalContext_foldlFrom___spec__3___rarg(lean_object*, lean_object*, size_t, size_t, lean_object*);
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__5(lean_object*);
|
||||
lean_object* l_Lean_LocalContext_findDecl_x3f___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_foldlM(lean_object*);
|
||||
lean_object* l_Lean_LocalContext_foldlFromM(lean_object*);
|
||||
|
|
@ -269,7 +272,7 @@ lean_object* l_Lean_LocalDecl_index(lean_object*);
|
|||
lean_object* l_Lean_LocalContext_forM___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_foldlFrom___spec__5___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_allM___spec__4___rarg___lambda__1___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findRevM_x3f___at_Lean_LocalContext_findDeclRev_x3f___spec__2___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__6___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_foldlFromM___at_Lean_LocalContext_foldlFrom___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_findDecl_x3f___rarg___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_foldl(lean_object*);
|
||||
|
|
@ -283,23 +286,23 @@ lean_object* l_PersistentArray_anyM___at_Lean_LocalContext_any___spec__1___boxed
|
|||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_all___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_local_ctx_get(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_foldlFromM___at_Lean_LocalContext_foldlFrom___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__3___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_isEmpty___boxed(lean_object*);
|
||||
lean_object* l_PersistentHashMap_insertAux___main___at_Lean_LocalContext_mkLocalDecl___spec__2(lean_object*, size_t, size_t, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_anyMAux___main___at_Lean_LocalContext_all___spec__2___boxed(lean_object*, lean_object*);
|
||||
lean_object* lean_panic_fn(lean_object*, lean_object*);
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_anyM___spec__5___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_all___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findRevM_x3f___at_Lean_LocalContext_findFromUserName_x3f___spec__1___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__3(lean_object*);
|
||||
lean_object* l_PersistentArray_findSomeRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__3(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findSomeRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__3___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_foldlFrom___spec__8___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_get_x21___closed__2;
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_anyM___spec__3(lean_object*);
|
||||
lean_object* l_Array_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__6___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_any___boxed(lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_LocalContext_1__popTailNoneAux(lean_object*);
|
||||
lean_object* l_Lean_LocalContext_mkLambda(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_allM___spec__5___boxed(lean_object*);
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__3___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_PersistentArray_anyMAux___main___at_Lean_LocalContext_all___spec__2(lean_object*, lean_object*);
|
||||
lean_object* l_Array_eraseIdx_x27___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_findDeclRevM_x3f___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -318,31 +321,32 @@ lean_object* l_PersistentArray_foldlFromM___at_Lean_LocalContext_foldlFrom___spe
|
|||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_anyM___spec__5___boxed(lean_object*);
|
||||
uint8_t l_Lean_LocalContext_any(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_get_x21___closed__1;
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__6___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_allM___spec__5___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
|
||||
lean_object* l_PersistentHashMap_insert___at_Lean_LocalContext_mkLocalDecl___spec__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_getCollisionNodeSize___rarg(lean_object*);
|
||||
lean_object* l_Lean_mkLet(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
|
||||
extern lean_object* l_Lean_Expr_Inhabited;
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__6(lean_object*);
|
||||
lean_object* l_Lean_LocalContext_foldlM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_all___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_getFVar_x21___boxed(lean_object*, lean_object*);
|
||||
lean_object* lean_expr_abstract(lean_object*, lean_object*);
|
||||
lean_object* l_Array_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__4(lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_foldlFrom___spec__7(lean_object*);
|
||||
lean_object* l_PersistentArray_findSomeRevM_x3f___at_Lean_LocalContext_findDeclRev_x3f___spec__2(lean_object*);
|
||||
lean_object* l_PersistentArray_findSomeM_x3f___at_Lean_LocalContext_findDecl_x3f___spec__2(lean_object*);
|
||||
lean_object* l_Lean_LocalContext_findDeclM_x3f___at_Lean_LocalContext_findDecl_x3f___spec__1___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findRevM_x3f___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__4(lean_object*);
|
||||
lean_object* l_Lean_LocalContext_foldl___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_allM___spec__3(lean_object*);
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__3(lean_object*);
|
||||
lean_object* l_Lean_LocalContext_findDeclM_x3f___at_Lean_LocalContext_findDecl_x3f___spec__1___rarg___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_erase___at_Lean_LocalContext_erase___spec__1___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_isSubPrefixOf___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Array_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__4___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_mkBinding___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__6(lean_object*);
|
||||
lean_object* l_PersistentArray_anyMAux___main___at_Lean_LocalContext_anyM___spec__2___boxed(lean_object*);
|
||||
lean_object* l_PersistentArray_findRevM_x3f___at_Lean_LocalContext_findDeclRev_x3f___spec__2(lean_object*);
|
||||
lean_object* l_PersistentArray_findSomeRevM_x3f___at_Lean_LocalContext_findFromUserName_x3f___spec__1___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_foldlFromM___at_Lean_LocalContext_foldlFrom___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__6___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_foldlFromM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_local_ctx_find(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_allM(lean_object*);
|
||||
|
|
@ -351,13 +355,11 @@ lean_object* l_Lean_LocalContext_anyM(lean_object*);
|
|||
lean_object* l_Lean_LocalContext_mkForall(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_usize_to_nat(size_t);
|
||||
lean_object* l_PersistentArray_foldlM___at_Lean_LocalContext_foldl___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__5___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_foldlMAux___main___at_Lean_LocalContext_foldlFrom___spec__4(lean_object*);
|
||||
lean_object* l_PersistentArray_foldlMAux___main___at_Lean_LocalContext_foldlFrom___spec__4___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_contains___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__4___rarg___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_foldlFrom___spec__9___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__5(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_anyM___at_Lean_LocalContext_allM___spec__1___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_foldlMAux___main___at_Lean_LocalContext_foldl___spec__3___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_anyM___spec__3___boxed(lean_object*);
|
||||
|
|
@ -368,12 +370,10 @@ uint8_t l_Lean_LocalContext_isSubPrefixOfAux___main(lean_object*, lean_object*,
|
|||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_allM___spec__5___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_set___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_foldlM___boxed(lean_object*);
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__4(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_containsFVar___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_allM___spec__4(lean_object*);
|
||||
lean_object* l_Lean_LocalContext_mkForall___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_allM___boxed(lean_object*);
|
||||
lean_object* l_PersistentArray_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__4___rarg(lean_object*, lean_object*);
|
||||
uint8_t l_Array_anyRangeMAux___main___at_Lean_LocalContext_all___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Lean_LocalDecl_isLet(lean_object*);
|
||||
lean_object* l_PersistentHashMap_containsAtAux___main___at_Lean_LocalContext_contains___spec__3___boxed(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -2844,7 +2844,7 @@ return x_1;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5; uint8_t x_6;
|
||||
|
|
@ -2895,7 +2895,7 @@ return x_10;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5; uint8_t x_6;
|
||||
|
|
@ -2915,7 +2915,7 @@ x_8 = lean_unsigned_to_nat(1u);
|
|||
x_9 = lean_nat_sub(x_3, x_8);
|
||||
lean_dec(x_3);
|
||||
x_10 = lean_array_fget(x_2, x_9);
|
||||
x_11 = l_PersistentArray_findRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__3(x_1, x_10);
|
||||
x_11 = l_PersistentArray_findSomeRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__3(x_1, x_10);
|
||||
lean_dec(x_10);
|
||||
if (lean_obj_tag(x_11) == 0)
|
||||
{
|
||||
|
|
@ -2931,7 +2931,7 @@ return x_11;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__5(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__5(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5; uint8_t x_6;
|
||||
|
|
@ -2982,7 +2982,7 @@ return x_10;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_PersistentArray_findRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__3(lean_object* x_1, lean_object* x_2) {
|
||||
lean_object* l_PersistentArray_findSomeRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__3(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
if (lean_obj_tag(x_2) == 0)
|
||||
|
|
@ -2990,7 +2990,7 @@ if (lean_obj_tag(x_2) == 0)
|
|||
lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_3 = lean_ctor_get(x_2, 0);
|
||||
x_4 = lean_array_get_size(x_3);
|
||||
x_5 = l_Array_findRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__4(x_1, x_3, x_4, lean_box(0));
|
||||
x_5 = l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__4(x_1, x_3, x_4, lean_box(0));
|
||||
return x_5;
|
||||
}
|
||||
else
|
||||
|
|
@ -2998,23 +2998,23 @@ else
|
|||
lean_object* x_6; lean_object* x_7; lean_object* x_8;
|
||||
x_6 = lean_ctor_get(x_2, 0);
|
||||
x_7 = lean_array_get_size(x_6);
|
||||
x_8 = l_Array_findRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__5(x_1, x_6, x_7, lean_box(0));
|
||||
x_8 = l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__5(x_1, x_6, x_7, lean_box(0));
|
||||
return x_8;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_PersistentArray_findRevM_x3f___at_Lean_LocalContext_findFromUserName_x3f___spec__1(lean_object* x_1, lean_object* x_2) {
|
||||
lean_object* l_PersistentArray_findSomeRevM_x3f___at_Lean_LocalContext_findFromUserName_x3f___spec__1(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_3 = lean_ctor_get(x_2, 1);
|
||||
x_4 = lean_array_get_size(x_3);
|
||||
x_5 = l_Array_findRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__2(x_1, x_3, x_4, lean_box(0));
|
||||
x_5 = l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__2(x_1, x_3, x_4, lean_box(0));
|
||||
if (lean_obj_tag(x_5) == 0)
|
||||
{
|
||||
lean_object* x_6; lean_object* x_7;
|
||||
x_6 = lean_ctor_get(x_2, 0);
|
||||
x_7 = l_PersistentArray_findRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__3(x_1, x_6);
|
||||
x_7 = l_PersistentArray_findSomeRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__3(x_1, x_6);
|
||||
return x_7;
|
||||
}
|
||||
else
|
||||
|
|
@ -3030,57 +3030,57 @@ lean_object* x_3; lean_object* x_4;
|
|||
x_3 = lean_ctor_get(x_1, 1);
|
||||
lean_inc(x_3);
|
||||
lean_dec(x_1);
|
||||
x_4 = l_PersistentArray_findRevM_x3f___at_Lean_LocalContext_findFromUserName_x3f___spec__1(x_2, x_3);
|
||||
x_4 = l_PersistentArray_findSomeRevM_x3f___at_Lean_LocalContext_findFromUserName_x3f___spec__1(x_2, x_3);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5;
|
||||
x_5 = l_Array_findRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__2(x_1, x_2, x_3, x_4);
|
||||
x_5 = l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__2(x_1, x_2, x_3, x_4);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__4___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__4___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5;
|
||||
x_5 = l_Array_findRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__4(x_1, x_2, x_3, x_4);
|
||||
x_5 = l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__4(x_1, x_2, x_3, x_4);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__5___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__5___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5;
|
||||
x_5 = l_Array_findRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__5(x_1, x_2, x_3, x_4);
|
||||
x_5 = l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__5(x_1, x_2, x_3, x_4);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_PersistentArray_findRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__3___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
lean_object* l_PersistentArray_findSomeRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__3___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l_PersistentArray_findRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__3(x_1, x_2);
|
||||
x_3 = l_PersistentArray_findSomeRevMAux___main___at_Lean_LocalContext_findFromUserName_x3f___spec__3(x_1, x_2);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_PersistentArray_findRevM_x3f___at_Lean_LocalContext_findFromUserName_x3f___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
lean_object* l_PersistentArray_findSomeRevM_x3f___at_Lean_LocalContext_findFromUserName_x3f___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l_PersistentArray_findRevM_x3f___at_Lean_LocalContext_findFromUserName_x3f___spec__1(x_1, x_2);
|
||||
x_3 = l_PersistentArray_findSomeRevM_x3f___at_Lean_LocalContext_findFromUserName_x3f___spec__1(x_1, x_2);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
return x_3;
|
||||
|
|
@ -3496,7 +3496,7 @@ lean_inc(x_1);
|
|||
x_6 = lean_alloc_closure((void*)(l_Lean_LocalContext_findDeclM_x3f___rarg___lambda__1), 3, 2);
|
||||
lean_closure_set(x_6, 0, x_1);
|
||||
lean_closure_set(x_6, 1, x_4);
|
||||
x_7 = l_PersistentArray_findM_x3f___rarg(x_1, lean_box(0), x_5, x_6);
|
||||
x_7 = l_PersistentArray_findSomeM_x3f___rarg(x_1, lean_box(0), x_5, x_6);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
|
|
@ -3528,7 +3528,7 @@ lean_inc(x_1);
|
|||
x_6 = lean_alloc_closure((void*)(l_Lean_LocalContext_findDeclM_x3f___rarg___lambda__1), 3, 2);
|
||||
lean_closure_set(x_6, 0, x_1);
|
||||
lean_closure_set(x_6, 1, x_4);
|
||||
x_7 = l_PersistentArray_findRevM_x3f___rarg(x_1, lean_box(0), x_5, x_6);
|
||||
x_7 = l_PersistentArray_findSomeRevM_x3f___rarg(x_1, lean_box(0), x_5, x_6);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
|
|
@ -3874,7 +3874,7 @@ lean_dec(x_1);
|
|||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__4___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__4___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4; uint8_t x_5;
|
||||
|
|
@ -3894,7 +3894,7 @@ else
|
|||
lean_object* x_7; lean_object* x_8;
|
||||
x_7 = lean_array_fget(x_2, x_3);
|
||||
lean_inc(x_1);
|
||||
x_8 = l_PersistentArray_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__3___rarg(x_1, x_7);
|
||||
x_8 = l_PersistentArray_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__3___rarg(x_1, x_7);
|
||||
lean_dec(x_7);
|
||||
if (lean_obj_tag(x_8) == 0)
|
||||
{
|
||||
|
|
@ -3914,15 +3914,15 @@ return x_8;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__4(lean_object* x_1) {
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__4(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = lean_alloc_closure((void*)(l_Array_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__4___rarg___boxed), 3, 0);
|
||||
x_2 = lean_alloc_closure((void*)(l_Array_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__4___rarg___boxed), 3, 0);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__5___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__5___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4; uint8_t x_5;
|
||||
|
|
@ -3977,15 +3977,15 @@ return x_12;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__5(lean_object* x_1) {
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__5(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = lean_alloc_closure((void*)(l_Array_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__5___rarg___boxed), 3, 0);
|
||||
x_2 = lean_alloc_closure((void*)(l_Array_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__5___rarg___boxed), 3, 0);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_PersistentArray_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__3___rarg(lean_object* x_1, lean_object* x_2) {
|
||||
lean_object* l_PersistentArray_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__3___rarg(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
if (lean_obj_tag(x_2) == 0)
|
||||
|
|
@ -3993,7 +3993,7 @@ if (lean_obj_tag(x_2) == 0)
|
|||
lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_3 = lean_ctor_get(x_2, 0);
|
||||
x_4 = lean_unsigned_to_nat(0u);
|
||||
x_5 = l_Array_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__4___rarg(x_1, x_3, x_4);
|
||||
x_5 = l_Array_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__4___rarg(x_1, x_3, x_4);
|
||||
return x_5;
|
||||
}
|
||||
else
|
||||
|
|
@ -4001,20 +4001,20 @@ else
|
|||
lean_object* x_6; lean_object* x_7; lean_object* x_8;
|
||||
x_6 = lean_ctor_get(x_2, 0);
|
||||
x_7 = lean_unsigned_to_nat(0u);
|
||||
x_8 = l_Array_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__5___rarg(x_1, x_6, x_7);
|
||||
x_8 = l_Array_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__5___rarg(x_1, x_6, x_7);
|
||||
return x_8;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_PersistentArray_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__3(lean_object* x_1) {
|
||||
lean_object* l_PersistentArray_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__3(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = lean_alloc_closure((void*)(l_PersistentArray_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__3___rarg___boxed), 2, 0);
|
||||
x_2 = lean_alloc_closure((void*)(l_PersistentArray_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__3___rarg___boxed), 2, 0);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__6___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__6___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4; uint8_t x_5;
|
||||
|
|
@ -4069,27 +4069,27 @@ return x_12;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__6(lean_object* x_1) {
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__6(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = lean_alloc_closure((void*)(l_Array_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__6___rarg___boxed), 3, 0);
|
||||
x_2 = lean_alloc_closure((void*)(l_Array_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__6___rarg___boxed), 3, 0);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_PersistentArray_findM_x3f___at_Lean_LocalContext_findDecl_x3f___spec__2___rarg(lean_object* x_1, lean_object* x_2) {
|
||||
lean_object* l_PersistentArray_findSomeM_x3f___at_Lean_LocalContext_findDecl_x3f___spec__2___rarg(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3; lean_object* x_4;
|
||||
x_3 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_1);
|
||||
x_4 = l_PersistentArray_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__3___rarg(x_1, x_3);
|
||||
x_4 = l_PersistentArray_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__3___rarg(x_1, x_3);
|
||||
if (lean_obj_tag(x_4) == 0)
|
||||
{
|
||||
lean_object* x_5; lean_object* x_6; lean_object* x_7;
|
||||
x_5 = lean_ctor_get(x_2, 1);
|
||||
x_6 = lean_unsigned_to_nat(0u);
|
||||
x_7 = l_Array_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__6___rarg(x_1, x_5, x_6);
|
||||
x_7 = l_Array_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__6___rarg(x_1, x_5, x_6);
|
||||
return x_7;
|
||||
}
|
||||
else
|
||||
|
|
@ -4099,11 +4099,11 @@ return x_4;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_PersistentArray_findM_x3f___at_Lean_LocalContext_findDecl_x3f___spec__2(lean_object* x_1) {
|
||||
lean_object* l_PersistentArray_findSomeM_x3f___at_Lean_LocalContext_findDecl_x3f___spec__2(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = lean_alloc_closure((void*)(l_PersistentArray_findM_x3f___at_Lean_LocalContext_findDecl_x3f___spec__2___rarg___boxed), 2, 0);
|
||||
x_2 = lean_alloc_closure((void*)(l_PersistentArray_findSomeM_x3f___at_Lean_LocalContext_findDecl_x3f___spec__2___rarg___boxed), 2, 0);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
|
|
@ -4112,7 +4112,7 @@ _start:
|
|||
{
|
||||
lean_object* x_3; lean_object* x_4;
|
||||
x_3 = lean_ctor_get(x_2, 1);
|
||||
x_4 = l_PersistentArray_findM_x3f___at_Lean_LocalContext_findDecl_x3f___spec__2___rarg(x_1, x_3);
|
||||
x_4 = l_PersistentArray_findSomeM_x3f___at_Lean_LocalContext_findDecl_x3f___spec__2___rarg(x_1, x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
|
|
@ -4140,47 +4140,47 @@ x_2 = lean_alloc_closure((void*)(l_Lean_LocalContext_findDecl_x3f___rarg___boxed
|
|||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__4___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__4___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = l_Array_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__4___rarg(x_1, x_2, x_3);
|
||||
x_4 = l_Array_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__4___rarg(x_1, x_2, x_3);
|
||||
lean_dec(x_2);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__5___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__5___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = l_Array_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__5___rarg(x_1, x_2, x_3);
|
||||
x_4 = l_Array_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__5___rarg(x_1, x_2, x_3);
|
||||
lean_dec(x_2);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_PersistentArray_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__3___rarg___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
lean_object* l_PersistentArray_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__3___rarg___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l_PersistentArray_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__3___rarg(x_1, x_2);
|
||||
x_3 = l_PersistentArray_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__3___rarg(x_1, x_2);
|
||||
lean_dec(x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__6___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__6___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = l_Array_findMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__6___rarg(x_1, x_2, x_3);
|
||||
x_4 = l_Array_findSomeMAux___main___at_Lean_LocalContext_findDecl_x3f___spec__6___rarg(x_1, x_2, x_3);
|
||||
lean_dec(x_2);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_PersistentArray_findM_x3f___at_Lean_LocalContext_findDecl_x3f___spec__2___rarg___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
lean_object* l_PersistentArray_findSomeM_x3f___at_Lean_LocalContext_findDecl_x3f___spec__2___rarg___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l_PersistentArray_findM_x3f___at_Lean_LocalContext_findDecl_x3f___spec__2___rarg(x_1, x_2);
|
||||
x_3 = l_PersistentArray_findSomeM_x3f___at_Lean_LocalContext_findDecl_x3f___spec__2___rarg(x_1, x_2);
|
||||
lean_dec(x_2);
|
||||
return x_3;
|
||||
}
|
||||
|
|
@ -4203,7 +4203,7 @@ lean_dec(x_1);
|
|||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__3___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__3___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5; uint8_t x_6;
|
||||
|
|
@ -4254,15 +4254,15 @@ return x_13;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__3(lean_object* x_1) {
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__3(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = lean_alloc_closure((void*)(l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__3___rarg___boxed), 4, 0);
|
||||
x_2 = lean_alloc_closure((void*)(l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__3___rarg___boxed), 4, 0);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__5___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__5___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5; uint8_t x_6;
|
||||
|
|
@ -4284,7 +4284,7 @@ x_9 = lean_nat_sub(x_3, x_8);
|
|||
lean_dec(x_3);
|
||||
x_10 = lean_array_fget(x_2, x_9);
|
||||
lean_inc(x_1);
|
||||
x_11 = l_PersistentArray_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__4___rarg(x_1, x_10);
|
||||
x_11 = l_PersistentArray_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__4___rarg(x_1, x_10);
|
||||
lean_dec(x_10);
|
||||
if (lean_obj_tag(x_11) == 0)
|
||||
{
|
||||
|
|
@ -4301,15 +4301,15 @@ return x_11;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__5(lean_object* x_1) {
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__5(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = lean_alloc_closure((void*)(l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__5___rarg___boxed), 4, 0);
|
||||
x_2 = lean_alloc_closure((void*)(l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__5___rarg___boxed), 4, 0);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__6___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__6___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5; uint8_t x_6;
|
||||
|
|
@ -4360,15 +4360,15 @@ return x_13;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__6(lean_object* x_1) {
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__6(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = lean_alloc_closure((void*)(l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__6___rarg___boxed), 4, 0);
|
||||
x_2 = lean_alloc_closure((void*)(l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__6___rarg___boxed), 4, 0);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_PersistentArray_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__4___rarg(lean_object* x_1, lean_object* x_2) {
|
||||
lean_object* l_PersistentArray_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__4___rarg(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
if (lean_obj_tag(x_2) == 0)
|
||||
|
|
@ -4376,7 +4376,7 @@ if (lean_obj_tag(x_2) == 0)
|
|||
lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_3 = lean_ctor_get(x_2, 0);
|
||||
x_4 = lean_array_get_size(x_3);
|
||||
x_5 = l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__5___rarg(x_1, x_3, x_4, lean_box(0));
|
||||
x_5 = l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__5___rarg(x_1, x_3, x_4, lean_box(0));
|
||||
return x_5;
|
||||
}
|
||||
else
|
||||
|
|
@ -4384,32 +4384,32 @@ else
|
|||
lean_object* x_6; lean_object* x_7; lean_object* x_8;
|
||||
x_6 = lean_ctor_get(x_2, 0);
|
||||
x_7 = lean_array_get_size(x_6);
|
||||
x_8 = l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__6___rarg(x_1, x_6, x_7, lean_box(0));
|
||||
x_8 = l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__6___rarg(x_1, x_6, x_7, lean_box(0));
|
||||
return x_8;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_PersistentArray_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__4(lean_object* x_1) {
|
||||
lean_object* l_PersistentArray_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__4(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = lean_alloc_closure((void*)(l_PersistentArray_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__4___rarg___boxed), 2, 0);
|
||||
x_2 = lean_alloc_closure((void*)(l_PersistentArray_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__4___rarg___boxed), 2, 0);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_PersistentArray_findRevM_x3f___at_Lean_LocalContext_findDeclRev_x3f___spec__2___rarg(lean_object* x_1, lean_object* x_2) {
|
||||
lean_object* l_PersistentArray_findSomeRevM_x3f___at_Lean_LocalContext_findDeclRev_x3f___spec__2___rarg(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_3 = lean_ctor_get(x_2, 1);
|
||||
x_4 = lean_array_get_size(x_3);
|
||||
lean_inc(x_1);
|
||||
x_5 = l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__3___rarg(x_1, x_3, x_4, lean_box(0));
|
||||
x_5 = l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__3___rarg(x_1, x_3, x_4, lean_box(0));
|
||||
if (lean_obj_tag(x_5) == 0)
|
||||
{
|
||||
lean_object* x_6; lean_object* x_7;
|
||||
x_6 = lean_ctor_get(x_2, 0);
|
||||
x_7 = l_PersistentArray_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__4___rarg(x_1, x_6);
|
||||
x_7 = l_PersistentArray_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__4___rarg(x_1, x_6);
|
||||
return x_7;
|
||||
}
|
||||
else
|
||||
|
|
@ -4419,11 +4419,11 @@ return x_5;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_PersistentArray_findRevM_x3f___at_Lean_LocalContext_findDeclRev_x3f___spec__2(lean_object* x_1) {
|
||||
lean_object* l_PersistentArray_findSomeRevM_x3f___at_Lean_LocalContext_findDeclRev_x3f___spec__2(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = lean_alloc_closure((void*)(l_PersistentArray_findRevM_x3f___at_Lean_LocalContext_findDeclRev_x3f___spec__2___rarg___boxed), 2, 0);
|
||||
x_2 = lean_alloc_closure((void*)(l_PersistentArray_findSomeRevM_x3f___at_Lean_LocalContext_findDeclRev_x3f___spec__2___rarg___boxed), 2, 0);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
|
|
@ -4432,7 +4432,7 @@ _start:
|
|||
{
|
||||
lean_object* x_3; lean_object* x_4;
|
||||
x_3 = lean_ctor_get(x_2, 1);
|
||||
x_4 = l_PersistentArray_findRevM_x3f___at_Lean_LocalContext_findDeclRev_x3f___spec__2___rarg(x_1, x_3);
|
||||
x_4 = l_PersistentArray_findSomeRevM_x3f___at_Lean_LocalContext_findDeclRev_x3f___spec__2___rarg(x_1, x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
|
|
@ -4460,47 +4460,47 @@ x_2 = lean_alloc_closure((void*)(l_Lean_LocalContext_findDeclRev_x3f___rarg___bo
|
|||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__3___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__3___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5;
|
||||
x_5 = l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__3___rarg(x_1, x_2, x_3, x_4);
|
||||
x_5 = l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__3___rarg(x_1, x_2, x_3, x_4);
|
||||
lean_dec(x_2);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__5___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__5___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5;
|
||||
x_5 = l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__5___rarg(x_1, x_2, x_3, x_4);
|
||||
x_5 = l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__5___rarg(x_1, x_2, x_3, x_4);
|
||||
lean_dec(x_2);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__6___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__6___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5;
|
||||
x_5 = l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__6___rarg(x_1, x_2, x_3, x_4);
|
||||
x_5 = l_Array_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__6___rarg(x_1, x_2, x_3, x_4);
|
||||
lean_dec(x_2);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_PersistentArray_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__4___rarg___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
lean_object* l_PersistentArray_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__4___rarg___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l_PersistentArray_findRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__4___rarg(x_1, x_2);
|
||||
x_3 = l_PersistentArray_findSomeRevMAux___main___at_Lean_LocalContext_findDeclRev_x3f___spec__4___rarg(x_1, x_2);
|
||||
lean_dec(x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_PersistentArray_findRevM_x3f___at_Lean_LocalContext_findDeclRev_x3f___spec__2___rarg___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
lean_object* l_PersistentArray_findSomeRevM_x3f___at_Lean_LocalContext_findDeclRev_x3f___spec__2___rarg___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l_PersistentArray_findRevM_x3f___at_Lean_LocalContext_findDeclRev_x3f___spec__2___rarg(x_1, x_2);
|
||||
x_3 = l_PersistentArray_findSomeRevM_x3f___at_Lean_LocalContext_findDeclRev_x3f___spec__2___rarg(x_1, x_2);
|
||||
lean_dec(x_2);
|
||||
return x_3;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -13,58 +13,58 @@
|
|||
#ifdef __cplusplus
|
||||
extern "C" {
|
||||
#endif
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__12___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_findDeclRevM_x3f___at_Lean_Meta_assumptionAux___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__10(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findRevM_x3f___at_Lean_Meta_assumptionAux___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findRevM_x3f___at_Lean_Meta_assumptionAux___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__12(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findSomeRevM_x3f___at_Lean_Meta_assumptionAux___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__10___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_assumption___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_array_get_size(lean_object*);
|
||||
lean_object* l_Lean_Meta_assumption___closed__1;
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__13(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findRevM_x3f___at_Lean_Meta_assumptionAux___spec__9(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__13___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Array_isEqvAux___main___at_Lean_Meta_assumptionAux___spec__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_nat_add(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_assumptionAux(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findRevM_x3f___at_Lean_Meta_assumptionAux___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_assumptionAux___closed__2;
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__10(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__11(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_array_fget(lean_object*, lean_object*);
|
||||
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_getMVarType(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_nat_sub(lean_object*, lean_object*);
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__12(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Format_join___closed__1;
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__13(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_name_mk_string(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__11___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalDecl_toExpr(lean_object*);
|
||||
lean_object* l_Lean_Meta_assumption(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__12___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_findDeclRevM_x3f___at_Lean_Meta_assumptionAux___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__10___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalDecl_type(lean_object*);
|
||||
lean_object* l_Lean_Meta_throwTacticEx___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__11___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_assignExprMVar(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_assumptionAux___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_assumptionAux___closed__1;
|
||||
lean_object* l_PersistentArray_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__4(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_checkNotAssigned(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_LocalContext_findDeclRevM_x3f___at_Lean_Meta_assumptionAux___spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findSomeRevM_x3f___at_Lean_Meta_assumptionAux___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findSomeRevM_x3f___at_Lean_Meta_assumptionAux___spec__9(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_isEqvAux___main___at_Lean_Meta_assumptionAux___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__4(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findSomeRevM_x3f___at_Lean_Meta_assumptionAux___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_isExprDefEq(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_getMVarDecl(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Lean_LocalInstance_beq(lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Meta_resettingSynthInstanceCache___rarg___closed__1;
|
||||
lean_object* l_Lean_LocalContext_findDeclRevM_x3f___at_Lean_Meta_assumptionAux___spec__8(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__13___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__11(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__3(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* l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__3(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; uint8_t x_8;
|
||||
|
|
@ -281,7 +281,7 @@ return x_48;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__5(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* l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__5(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; uint8_t x_8;
|
||||
|
|
@ -308,7 +308,7 @@ lean_dec(x_3);
|
|||
x_13 = lean_array_fget(x_2, x_12);
|
||||
lean_inc(x_5);
|
||||
lean_inc(x_1);
|
||||
x_14 = l_PersistentArray_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__4(x_1, x_13, x_5, x_6);
|
||||
x_14 = l_PersistentArray_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__4(x_1, x_13, x_5, x_6);
|
||||
lean_dec(x_13);
|
||||
if (lean_obj_tag(x_14) == 0)
|
||||
{
|
||||
|
|
@ -381,7 +381,7 @@ return x_25;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__6(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* l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__6(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; uint8_t x_8;
|
||||
|
|
@ -598,7 +598,7 @@ return x_48;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_PersistentArray_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_PersistentArray_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
if (lean_obj_tag(x_2) == 0)
|
||||
|
|
@ -606,7 +606,7 @@ if (lean_obj_tag(x_2) == 0)
|
|||
lean_object* x_5; lean_object* x_6; lean_object* x_7;
|
||||
x_5 = lean_ctor_get(x_2, 0);
|
||||
x_6 = lean_array_get_size(x_5);
|
||||
x_7 = l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__5(x_1, x_5, x_6, lean_box(0), x_3, x_4);
|
||||
x_7 = l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__5(x_1, x_5, x_6, lean_box(0), x_3, x_4);
|
||||
return x_7;
|
||||
}
|
||||
else
|
||||
|
|
@ -614,12 +614,12 @@ else
|
|||
lean_object* x_8; lean_object* x_9; lean_object* x_10;
|
||||
x_8 = lean_ctor_get(x_2, 0);
|
||||
x_9 = lean_array_get_size(x_8);
|
||||
x_10 = l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__6(x_1, x_8, x_9, lean_box(0), x_3, x_4);
|
||||
x_10 = l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__6(x_1, x_8, x_9, lean_box(0), x_3, x_4);
|
||||
return x_10;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_PersistentArray_findRevM_x3f___at_Lean_Meta_assumptionAux___spec__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_PersistentArray_findSomeRevM_x3f___at_Lean_Meta_assumptionAux___spec__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5; lean_object* x_6; lean_object* x_7;
|
||||
|
|
@ -627,7 +627,7 @@ x_5 = lean_ctor_get(x_2, 1);
|
|||
x_6 = lean_array_get_size(x_5);
|
||||
lean_inc(x_3);
|
||||
lean_inc(x_1);
|
||||
x_7 = l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__3(x_1, x_5, x_6, lean_box(0), x_3, x_4);
|
||||
x_7 = l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__3(x_1, x_5, x_6, lean_box(0), x_3, x_4);
|
||||
if (lean_obj_tag(x_7) == 0)
|
||||
{
|
||||
lean_object* x_8;
|
||||
|
|
@ -640,7 +640,7 @@ x_9 = lean_ctor_get(x_7, 1);
|
|||
lean_inc(x_9);
|
||||
lean_dec(x_7);
|
||||
x_10 = lean_ctor_get(x_2, 0);
|
||||
x_11 = l_PersistentArray_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__4(x_1, x_10, x_3, x_9);
|
||||
x_11 = l_PersistentArray_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__4(x_1, x_10, x_3, x_9);
|
||||
return x_11;
|
||||
}
|
||||
else
|
||||
|
|
@ -700,7 +700,7 @@ _start:
|
|||
{
|
||||
lean_object* x_5; lean_object* x_6;
|
||||
x_5 = lean_ctor_get(x_2, 1);
|
||||
x_6 = l_PersistentArray_findRevM_x3f___at_Lean_Meta_assumptionAux___spec__2(x_1, x_5, x_3, x_4);
|
||||
x_6 = l_PersistentArray_findSomeRevM_x3f___at_Lean_Meta_assumptionAux___spec__2(x_1, x_5, x_3, x_4);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
|
|
@ -746,7 +746,7 @@ goto _start;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__10(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* l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__10(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; uint8_t x_8;
|
||||
|
|
@ -963,7 +963,7 @@ return x_48;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__12(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* l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__12(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; uint8_t x_8;
|
||||
|
|
@ -990,7 +990,7 @@ lean_dec(x_3);
|
|||
x_13 = lean_array_fget(x_2, x_12);
|
||||
lean_inc(x_5);
|
||||
lean_inc(x_1);
|
||||
x_14 = l_PersistentArray_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__11(x_1, x_13, x_5, x_6);
|
||||
x_14 = l_PersistentArray_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__11(x_1, x_13, x_5, x_6);
|
||||
lean_dec(x_13);
|
||||
if (lean_obj_tag(x_14) == 0)
|
||||
{
|
||||
|
|
@ -1063,7 +1063,7 @@ return x_25;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__13(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* l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__13(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; uint8_t x_8;
|
||||
|
|
@ -1280,7 +1280,7 @@ return x_48;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_PersistentArray_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__11(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_PersistentArray_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__11(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
if (lean_obj_tag(x_2) == 0)
|
||||
|
|
@ -1288,7 +1288,7 @@ if (lean_obj_tag(x_2) == 0)
|
|||
lean_object* x_5; lean_object* x_6; lean_object* x_7;
|
||||
x_5 = lean_ctor_get(x_2, 0);
|
||||
x_6 = lean_array_get_size(x_5);
|
||||
x_7 = l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__12(x_1, x_5, x_6, lean_box(0), x_3, x_4);
|
||||
x_7 = l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__12(x_1, x_5, x_6, lean_box(0), x_3, x_4);
|
||||
return x_7;
|
||||
}
|
||||
else
|
||||
|
|
@ -1296,12 +1296,12 @@ else
|
|||
lean_object* x_8; lean_object* x_9; lean_object* x_10;
|
||||
x_8 = lean_ctor_get(x_2, 0);
|
||||
x_9 = lean_array_get_size(x_8);
|
||||
x_10 = l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__13(x_1, x_8, x_9, lean_box(0), x_3, x_4);
|
||||
x_10 = l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__13(x_1, x_8, x_9, lean_box(0), x_3, x_4);
|
||||
return x_10;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_PersistentArray_findRevM_x3f___at_Lean_Meta_assumptionAux___spec__9(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_PersistentArray_findSomeRevM_x3f___at_Lean_Meta_assumptionAux___spec__9(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5; lean_object* x_6; lean_object* x_7;
|
||||
|
|
@ -1309,7 +1309,7 @@ x_5 = lean_ctor_get(x_2, 1);
|
|||
x_6 = lean_array_get_size(x_5);
|
||||
lean_inc(x_3);
|
||||
lean_inc(x_1);
|
||||
x_7 = l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__10(x_1, x_5, x_6, lean_box(0), x_3, x_4);
|
||||
x_7 = l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__10(x_1, x_5, x_6, lean_box(0), x_3, x_4);
|
||||
if (lean_obj_tag(x_7) == 0)
|
||||
{
|
||||
lean_object* x_8;
|
||||
|
|
@ -1322,7 +1322,7 @@ x_9 = lean_ctor_get(x_7, 1);
|
|||
lean_inc(x_9);
|
||||
lean_dec(x_7);
|
||||
x_10 = lean_ctor_get(x_2, 0);
|
||||
x_11 = l_PersistentArray_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__11(x_1, x_10, x_3, x_9);
|
||||
x_11 = l_PersistentArray_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__11(x_1, x_10, x_3, x_9);
|
||||
return x_11;
|
||||
}
|
||||
else
|
||||
|
|
@ -1382,7 +1382,7 @@ _start:
|
|||
{
|
||||
lean_object* x_5; lean_object* x_6;
|
||||
x_5 = lean_ctor_get(x_2, 1);
|
||||
x_6 = l_PersistentArray_findRevM_x3f___at_Lean_Meta_assumptionAux___spec__9(x_1, x_5, x_3, x_4);
|
||||
x_6 = l_PersistentArray_findSomeRevM_x3f___at_Lean_Meta_assumptionAux___spec__9(x_1, x_5, x_3, x_4);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
|
|
@ -2621,47 +2621,47 @@ return x_279;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_7;
|
||||
x_7 = l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__3(x_1, x_2, x_3, x_4, x_5, x_6);
|
||||
x_7 = l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__3(x_1, x_2, x_3, x_4, x_5, x_6);
|
||||
lean_dec(x_2);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__5___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__5___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_7;
|
||||
x_7 = l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__5(x_1, x_2, x_3, x_4, x_5, x_6);
|
||||
x_7 = l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__5(x_1, x_2, x_3, x_4, x_5, x_6);
|
||||
lean_dec(x_2);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__6___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__6___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_7;
|
||||
x_7 = l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__6(x_1, x_2, x_3, x_4, x_5, x_6);
|
||||
x_7 = l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__6(x_1, x_2, x_3, x_4, x_5, x_6);
|
||||
lean_dec(x_2);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
lean_object* l_PersistentArray_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__4___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_PersistentArray_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__4___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5;
|
||||
x_5 = l_PersistentArray_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__4(x_1, x_2, x_3, x_4);
|
||||
x_5 = l_PersistentArray_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__4(x_1, x_2, x_3, x_4);
|
||||
lean_dec(x_2);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_PersistentArray_findRevM_x3f___at_Lean_Meta_assumptionAux___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_PersistentArray_findSomeRevM_x3f___at_Lean_Meta_assumptionAux___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5;
|
||||
x_5 = l_PersistentArray_findRevM_x3f___at_Lean_Meta_assumptionAux___spec__2(x_1, x_2, x_3, x_4);
|
||||
x_5 = l_PersistentArray_findSomeRevM_x3f___at_Lean_Meta_assumptionAux___spec__2(x_1, x_2, x_3, x_4);
|
||||
lean_dec(x_2);
|
||||
return x_5;
|
||||
}
|
||||
|
|
@ -2688,47 +2688,47 @@ x_8 = lean_box(x_7);
|
|||
return x_8;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__10___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__10___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_7;
|
||||
x_7 = l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__10(x_1, x_2, x_3, x_4, x_5, x_6);
|
||||
x_7 = l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__10(x_1, x_2, x_3, x_4, x_5, x_6);
|
||||
lean_dec(x_2);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__12___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__12___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_7;
|
||||
x_7 = l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__12(x_1, x_2, x_3, x_4, x_5, x_6);
|
||||
x_7 = l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__12(x_1, x_2, x_3, x_4, x_5, x_6);
|
||||
lean_dec(x_2);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__13___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__13___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_7;
|
||||
x_7 = l_Array_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__13(x_1, x_2, x_3, x_4, x_5, x_6);
|
||||
x_7 = l_Array_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__13(x_1, x_2, x_3, x_4, x_5, x_6);
|
||||
lean_dec(x_2);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
lean_object* l_PersistentArray_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__11___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_PersistentArray_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__11___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5;
|
||||
x_5 = l_PersistentArray_findRevMAux___main___at_Lean_Meta_assumptionAux___spec__11(x_1, x_2, x_3, x_4);
|
||||
x_5 = l_PersistentArray_findSomeRevMAux___main___at_Lean_Meta_assumptionAux___spec__11(x_1, x_2, x_3, x_4);
|
||||
lean_dec(x_2);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_PersistentArray_findRevM_x3f___at_Lean_Meta_assumptionAux___spec__9___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_PersistentArray_findSomeRevM_x3f___at_Lean_Meta_assumptionAux___spec__9___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5;
|
||||
x_5 = l_PersistentArray_findRevM_x3f___at_Lean_Meta_assumptionAux___spec__9(x_1, x_2, x_3, x_4);
|
||||
x_5 = l_PersistentArray_findSomeRevM_x3f___at_Lean_Meta_assumptionAux___spec__9(x_1, x_2, x_3, x_4);
|
||||
lean_dec(x_2);
|
||||
return x_5;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -19,6 +19,7 @@ lean_object* l_Lean_getStructureCtor___closed__1;
|
|||
lean_object* l_Lean_getStructureCtor___closed__2;
|
||||
lean_object* l___private_Init_Lean_Structure_4__hasProjFn___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l___private_Init_Lean_Structure_4__hasProjFn(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_findField_x3f___main___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_getStructureCtor___closed__4;
|
||||
uint8_t lean_name_eq(lean_object*, lean_object*);
|
||||
extern lean_object* l_Array_empty___closed__1;
|
||||
|
|
@ -29,7 +30,6 @@ lean_object* lean_array_push(lean_object*, lean_object*);
|
|||
lean_object* lean_array_get_size(lean_object*);
|
||||
uint8_t l_Lean_isInternalSubobjectFieldName(lean_object*);
|
||||
lean_object* l___private_Init_Lean_Structure_2__isSubobjectFieldAux___main(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findMAux___main___at_Lean_findField_x3f___main___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Expr_getAppFn___main(lean_object*);
|
||||
lean_object* l_Array_contains___at_Lean_findField_x3f___main___spec__1___boxed(lean_object*, lean_object*);
|
||||
uint8_t l_Lean_Environment_isProjectionFn(lean_object*, lean_object*);
|
||||
|
|
@ -43,27 +43,27 @@ lean_object* l_Lean_getStructureFieldsFlattened(lean_object*, lean_object*);
|
|||
lean_object* l___private_Init_Lean_Structure_3__getStructureFieldsFlattenedAux(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_getStructureCtor___closed__5;
|
||||
lean_object* l_Lean_getStructureCtor___closed__3;
|
||||
lean_object* l_Array_findMAux___main___at_Lean_findField_x3f___main___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Array_anyRangeMAux___main___at_Lean_findField_x3f___main___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_name_mk_string(lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_Structure_1__getStructureFieldsAux___main(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_getStructureFields(lean_object*, lean_object*);
|
||||
lean_object* l_Array_findMAux___main___at_Lean_getPathToBaseStructureAux___main___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint32_t lean_string_utf8_get(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_getPathToBaseStructure_x3f(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_findField_x3f___main___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Array_contains___at_Lean_findField_x3f___main___spec__1(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_getPathToBaseStructureAux___main(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_Structure_1__getStructureFieldsAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l___private_Init_Lean_Structure_4__hasProjFn___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_getParentStructures___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_UInt32_decEq(uint32_t, uint32_t);
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_getPathToBaseStructureAux___main___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_getParentStructures(lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_Structure_2__isSubobjectFieldAux(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findMAux___main___at_Lean_getPathToBaseStructureAux___main___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_mkInternalSubobjectFieldName(lean_object*);
|
||||
lean_object* l___private_Init_Lean_Structure_2__isSubobjectFieldAux___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_Structure_2__isSubobjectFieldAux___main___closed__1;
|
||||
lean_object* l___private_Init_Lean_Structure_2__isSubobjectFieldAux___main___closed__2;
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_getPathToBaseStructureAux___main___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_findField_x3f___main___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_panic_fn(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_getStructureCtor(lean_object*, lean_object*);
|
||||
|
|
@ -811,7 +811,7 @@ lean_dec(x_3);
|
|||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findMAux___main___at_Lean_findField_x3f___main___spec__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_findField_x3f___main___spec__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5; uint8_t x_6;
|
||||
|
|
@ -865,7 +865,7 @@ lean_object* x_6; lean_object* x_7; lean_object* x_8;
|
|||
lean_inc(x_1);
|
||||
x_6 = l_Lean_getParentStructures(x_1, x_2);
|
||||
x_7 = lean_unsigned_to_nat(0u);
|
||||
x_8 = l_Array_findMAux___main___at_Lean_findField_x3f___main___spec__3(x_1, x_3, x_6, x_7);
|
||||
x_8 = l_Array_findSomeMAux___main___at_Lean_findField_x3f___main___spec__3(x_1, x_3, x_6, x_7);
|
||||
lean_dec(x_6);
|
||||
return x_8;
|
||||
}
|
||||
|
|
@ -903,11 +903,11 @@ x_4 = lean_box(x_3);
|
|||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findMAux___main___at_Lean_findField_x3f___main___spec__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_findField_x3f___main___spec__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5;
|
||||
x_5 = l_Array_findMAux___main___at_Lean_findField_x3f___main___spec__3(x_1, x_2, x_3, x_4);
|
||||
x_5 = l_Array_findSomeMAux___main___at_Lean_findField_x3f___main___spec__3(x_1, x_2, x_3, x_4);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
return x_5;
|
||||
|
|
@ -1148,7 +1148,7 @@ x_4 = lean_box(x_3);
|
|||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findMAux___main___at_Lean_getPathToBaseStructureAux___main___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_getPathToBaseStructureAux___main___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_7; uint8_t x_8;
|
||||
|
|
@ -1229,7 +1229,7 @@ lean_inc(x_3);
|
|||
lean_inc(x_1);
|
||||
x_6 = l_Lean_getStructureFields(x_1, x_3);
|
||||
x_7 = lean_unsigned_to_nat(0u);
|
||||
x_8 = l_Array_findMAux___main___at_Lean_getPathToBaseStructureAux___main___spec__1(x_1, x_2, x_3, x_4, x_6, x_7);
|
||||
x_8 = l_Array_findSomeMAux___main___at_Lean_getPathToBaseStructureAux___main___spec__1(x_1, x_2, x_3, x_4, x_6, x_7);
|
||||
lean_dec(x_6);
|
||||
return x_8;
|
||||
}
|
||||
|
|
@ -1245,11 +1245,11 @@ return x_10;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findMAux___main___at_Lean_getPathToBaseStructureAux___main___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_getPathToBaseStructureAux___main___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_7;
|
||||
x_7 = l_Array_findMAux___main___at_Lean_getPathToBaseStructureAux___main___spec__1(x_1, x_2, x_3, x_4, x_5, x_6);
|
||||
x_7 = l_Array_findSomeMAux___main___at_Lean_getPathToBaseStructureAux___main___spec__1(x_1, x_2, x_3, x_4, x_5, x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_2);
|
||||
return x_7;
|
||||
|
|
|
|||
|
|
@ -28,10 +28,8 @@ lean_object* l_Lean_Syntax_modifyArg(lean_object*, lean_object*, lean_object*);
|
|||
lean_object* l_Lean_Syntax_formatStxAux___main___closed__5;
|
||||
lean_object* l_Lean_Syntax_ifNodeKind___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t lean_name_eq(lean_object*, lean_object*);
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Syntax_getTailWithInfo___main___spec__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_mrewriteBottomUp___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_getIdAt(lean_object*, lean_object*);
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Syntax_getTailWithInfo___main___spec__1___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_HasToString;
|
||||
extern lean_object* l_Array_empty___closed__1;
|
||||
lean_object* l_Lean_SyntaxNode_withArgs(lean_object*);
|
||||
|
|
@ -71,7 +69,6 @@ lean_object* l_Lean_Syntax_formatStxAux___main___closed__8;
|
|||
lean_object* l_Lean_Syntax_ifNode(lean_object*);
|
||||
lean_object* l_Lean_Syntax_getTailWithInfo___main(lean_object*);
|
||||
lean_object* l_Lean_Syntax_formatStxAux___main___closed__4;
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Syntax_getTailInfo___main___spec__1___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_SyntaxNode_getIdAt(lean_object*, lean_object*);
|
||||
lean_object* lean_array_fget(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_SyntaxNode_getKind___boxed(lean_object*);
|
||||
|
|
@ -83,6 +80,7 @@ lean_object* l_Lean_Syntax_mreplace___main___rarg(lean_object*, lean_object*, le
|
|||
lean_object* lean_nat_sub(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_formatStxAux___main___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_Syntax_reprint___main___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_Syntax_getTailInfo___main___spec__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_List_map___main___at_Lean_Syntax_formatStxAux___main___spec__5___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_unreachIsNodeMissing(lean_object*, lean_object*);
|
||||
|
|
@ -108,8 +106,10 @@ lean_object* l_Array_umapMAux___main___at_Lean_Syntax_rewriteBottomUp___spec__2(
|
|||
lean_object* l_Lean_Syntax_isMissing___boxed(lean_object*);
|
||||
lean_object* l_Lean_Syntax_mreplace(lean_object*);
|
||||
lean_object* l___private_Init_Lean_Syntax_3__updateLast___main(lean_object*);
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_Syntax_getTailWithInfo___main___spec__1___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_SyntaxNode_modifyArgs(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_SyntaxNode_getArgs___boxed(lean_object*);
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_Syntax_getTailInfo___main___spec__1___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_List_map___main___at_Lean_Syntax_formatStxAux___main___spec__4(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_unreachIsNodeIdent___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_String_Iterator_HasRepr___closed__2;
|
||||
|
|
@ -154,6 +154,7 @@ extern lean_object* l_Lean_Format_paren___closed__2;
|
|||
lean_object* l_Lean_unreachIsNodeAtom___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_Syntax_3__updateLast___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_List_map___main___at_Lean_Syntax_formatStxAux___main___spec__4___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_Syntax_getTailWithInfo___main___spec__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_setTailInfoAux___main(lean_object*, lean_object*);
|
||||
lean_object* lean_format_group(lean_object*);
|
||||
lean_object* l_Lean_mkStxStrLit(lean_object*, lean_object*);
|
||||
|
|
@ -163,7 +164,6 @@ lean_object* lean_mk_syntax_num_lit(lean_object*);
|
|||
lean_object* l_Array_iterateMAux___main___at_Lean_Syntax_reprint___main___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_Syntax_updateLeading___spec__2(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_HasToString___closed__1;
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Syntax_getTailInfo___main___spec__1(lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_mkOptionalNode___closed__1;
|
||||
lean_object* l_Lean_Syntax_mrewriteBottomUp___main(lean_object*);
|
||||
lean_object* l_Lean_SyntaxNode_getIdAt___boxed(lean_object*, lean_object*);
|
||||
|
|
@ -2384,7 +2384,7 @@ lean_dec(x_1);
|
|||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Syntax_getTailWithInfo___main___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_Syntax_getTailWithInfo___main___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4; uint8_t x_5;
|
||||
|
|
@ -2436,7 +2436,7 @@ x_3 = lean_ctor_get(x_1, 1);
|
|||
lean_inc(x_3);
|
||||
lean_dec(x_1);
|
||||
x_4 = lean_array_get_size(x_3);
|
||||
x_5 = l_Array_findRevMAux___main___at_Lean_Syntax_getTailWithInfo___main___spec__1(x_3, x_4, lean_box(0));
|
||||
x_5 = l_Array_findSomeRevMAux___main___at_Lean_Syntax_getTailWithInfo___main___spec__1(x_3, x_4, lean_box(0));
|
||||
lean_dec(x_3);
|
||||
return x_5;
|
||||
}
|
||||
|
|
@ -2477,11 +2477,11 @@ return x_10;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Syntax_getTailWithInfo___main___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_Syntax_getTailWithInfo___main___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = l_Array_findRevMAux___main___at_Lean_Syntax_getTailWithInfo___main___spec__1(x_1, x_2, x_3);
|
||||
x_4 = l_Array_findSomeRevMAux___main___at_Lean_Syntax_getTailWithInfo___main___spec__1(x_1, x_2, x_3);
|
||||
lean_dec(x_1);
|
||||
return x_4;
|
||||
}
|
||||
|
|
@ -2494,7 +2494,7 @@ x_2 = l_Lean_Syntax_getTailWithInfo___main(x_1);
|
|||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Syntax_getTailInfo___main___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_Syntax_getTailInfo___main___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4; uint8_t x_5;
|
||||
|
|
@ -2545,7 +2545,7 @@ case 1:
|
|||
lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_3 = lean_ctor_get(x_1, 1);
|
||||
x_4 = lean_array_get_size(x_3);
|
||||
x_5 = l_Array_findRevMAux___main___at_Lean_Syntax_getTailInfo___main___spec__1(x_3, x_4, lean_box(0));
|
||||
x_5 = l_Array_findSomeRevMAux___main___at_Lean_Syntax_getTailInfo___main___spec__1(x_3, x_4, lean_box(0));
|
||||
return x_5;
|
||||
}
|
||||
default:
|
||||
|
|
@ -2558,11 +2558,11 @@ return x_6;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Syntax_getTailInfo___main___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
lean_object* l_Array_findSomeRevMAux___main___at_Lean_Syntax_getTailInfo___main___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = l_Array_findRevMAux___main___at_Lean_Syntax_getTailInfo___main___spec__1(x_1, x_2, x_3);
|
||||
x_4 = l_Array_findSomeRevMAux___main___at_Lean_Syntax_getTailInfo___main___spec__1(x_1, x_2, x_3);
|
||||
lean_dec(x_1);
|
||||
return x_4;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -27,12 +27,13 @@ lean_object* l_Lean_extractMacroScopes(lean_object*);
|
|||
lean_object* l_Lean_ParserDescr_pushLeading;
|
||||
lean_object* l_Lean_fieldIdxKind;
|
||||
lean_object* l_Lean_Syntax_isNatLit_x3f___boxed(lean_object*);
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_Syntax_getHeadInfo___main___spec__1(lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_LeanInit_1__eraseMacroScopesAux___main___closed__1;
|
||||
lean_object* l_Lean_MacroM_monadQuotation;
|
||||
lean_object* l_Lean_Name_eraseMacroScopes(lean_object*);
|
||||
lean_object* l_Lean_Syntax_isNatLitAux(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Macro_throwUnsupported___closed__1;
|
||||
lean_object* l_Array_findMAux___main___at_Lean_Syntax_getHeadInfo___main___spec__1___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Array_mapSepElemsM___boxed(lean_object*);
|
||||
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
|
||||
lean_object* l___private_Init_LeanInit_12__decodeQuotedChar___boxed__const__1;
|
||||
lean_object* l_Lean_MacroScopesView_inhabited;
|
||||
|
|
@ -51,17 +52,20 @@ lean_object* l_Lean_ParserDescr_orelse(uint8_t, lean_object*, lean_object*);
|
|||
lean_object* l_Lean_MacroM_monadQuotation___lambda__2(lean_object*);
|
||||
lean_object* l___private_Init_LeanInit_8__decodeHexDigit___boxed(lean_object*, lean_object*);
|
||||
uint32_t l_Lean_idBeginEscape;
|
||||
lean_object* l___private_Init_LeanInit_15__mapSepElemsMAux___boxed(lean_object*);
|
||||
lean_object* l___private_Init_LeanInit_10__decodeDecimalLitAux___main(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_LeanInit_4__extractMainModule(lean_object*, lean_object*, lean_object*);
|
||||
uint8_t lean_name_eq(lean_object*, lean_object*);
|
||||
lean_object* l_Array_findMAux___main___at_Lean_Syntax_getHeadInfo___main___spec__1(lean_object*, lean_object*);
|
||||
lean_object* l_Array_filterSepElemsM___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_isAtom___boxed(lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_optional(uint8_t, lean_object*);
|
||||
lean_object* l_Array_mapSepElemsM___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_toNat___boxed(lean_object*);
|
||||
lean_object* l_Lean_identKind___closed__2;
|
||||
lean_object* l___private_Init_LeanInit_8__decodeHexDigit(lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_LeanInit_1__eraseMacroScopesAux___main(lean_object*);
|
||||
lean_object* l___private_Init_LeanInit_15__mapSepElemsMAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_LeanInit_15__mapSepElemsMAux(lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_lookahead(uint8_t, lean_object*);
|
||||
lean_object* l___private_Init_LeanInit_5__extractMacroScopesAux(lean_object*, lean_object*);
|
||||
extern lean_object* l_Array_empty___closed__1;
|
||||
|
|
@ -69,6 +73,7 @@ lean_object* l_Lean_Syntax_isOfKind___boxed(lean_object*, lean_object*);
|
|||
lean_object* l_Lean_Name_HasBeq;
|
||||
lean_object* l___private_Init_LeanInit_13__decodeNameLitAux___main(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_fieldIdxKind___closed__1;
|
||||
lean_object* l___private_Init_LeanInit_15__mapSepElemsMAux___main(lean_object*);
|
||||
uint8_t l_Char_isDigit(uint32_t);
|
||||
lean_object* l_Lean_charLitKind___closed__2;
|
||||
lean_object* l_Lean_ParserDescr_many(uint8_t, lean_object*);
|
||||
|
|
@ -121,6 +126,7 @@ lean_object* l_Substring_takeWhileAux___main___at___private_Init_LeanInit_13__de
|
|||
lean_object* l_Lean_mkAppStx___closed__7;
|
||||
lean_object* lean_nat_add(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_isSubScriptAlnum___boxed(lean_object*);
|
||||
lean_object* l_Array_mapSepElems(lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_LeanInit_4__extractMainModule___main(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_foldlStepMAux___main___at_Array_getSepElems___spec__1(lean_object*);
|
||||
lean_object* l_Lean_Name_toStringWithSep(lean_object*, lean_object*);
|
||||
|
|
@ -131,17 +137,20 @@ lean_object* l_Lean_Name_hashable;
|
|||
lean_object* l_Lean_mkTermIdFromIdent___closed__2;
|
||||
lean_object* l_Lean_Syntax_isSimpleTermId_x3f(lean_object*, uint8_t);
|
||||
lean_object* lean_string_utf8_next(lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_LeanInit_15__mapSepElemsMAux___main___boxed(lean_object*);
|
||||
lean_object* l_Lean_Syntax_strLitToAtom(lean_object*);
|
||||
lean_object* l_Lean_Syntax_isLit_x3f___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_hasArgs___boxed(lean_object*);
|
||||
lean_object* l_Lean_mkStxNumLit(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_ParserDescrCore_inhabited(uint8_t);
|
||||
lean_object* l_Lean_Name_HasAppend___closed__1;
|
||||
lean_object* l_Array_mapSepElems___boxed(lean_object*, lean_object*);
|
||||
uint8_t l_Lean_Name_hasMacroScopes(lean_object*);
|
||||
lean_object* l_Lean_MacroM_monadQuotation___lambda__3(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_isLit_x3f(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_termIdToAntiquot___closed__4;
|
||||
lean_object* l_Lean_ParserDescr_many1(uint8_t, lean_object*);
|
||||
lean_object* l___private_Init_LeanInit_15__mapSepElemsMAux___main___at_Array_mapSepElems___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_isCharLit_x3f(lean_object*);
|
||||
lean_object* lean_array_fget(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_isNatLit_x3f(lean_object*);
|
||||
|
|
@ -152,6 +161,7 @@ lean_object* l_Lean_numLitKind;
|
|||
lean_object* l_Lean_ParserDescr_many___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_choiceKind___closed__1;
|
||||
lean_object* l___private_Init_LeanInit_7__decodeOctalLitAux___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_mapSepElemsM(lean_object*);
|
||||
lean_object* lean_nat_sub(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_choiceKind___closed__2;
|
||||
lean_object* l_Lean_MacroM_monadQuotation___lambda__2___boxed(lean_object*);
|
||||
|
|
@ -178,6 +188,7 @@ lean_object* l_Lean_numLitKind___closed__1;
|
|||
lean_object* l_Lean_NameGenerator_next(lean_object*);
|
||||
lean_object* l_Lean_Syntax_decodeCharLit___boxed(lean_object*);
|
||||
lean_object* l___private_Init_LeanInit_1__eraseMacroScopesAux(lean_object*);
|
||||
lean_object* l___private_Init_LeanInit_15__mapSepElemsMAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_strLitKind___closed__1;
|
||||
lean_object* l___private_Init_LeanInit_12__decodeQuotedChar___boxed__const__5;
|
||||
lean_object* l_Lean_Syntax_isNatLitAux___boxed(lean_object*, lean_object*);
|
||||
|
|
@ -193,6 +204,7 @@ lean_object* l_Lean_NameGenerator_Inhabited___closed__1;
|
|||
size_t l_Lean_Name_hash(lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_parser(uint8_t, lean_object*, lean_object*);
|
||||
lean_object* l_Nat_repr(lean_object*);
|
||||
lean_object* l_Array_mapSepElemsM___at_Array_mapSepElems___spec__1___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Name_HasToString;
|
||||
lean_object* l___private_Init_LeanInit_13__decodeNameLitAux___main___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_lookahead___boxed(lean_object*, lean_object*);
|
||||
|
|
@ -206,6 +218,7 @@ lean_object* l_Lean_ParserDescr_andthen(uint8_t, lean_object*, lean_object*);
|
|||
lean_object* l_Lean_ParserDescr_charLit___boxed(lean_object*);
|
||||
lean_object* l___private_Init_LeanInit_6__decodeBinLitAux___main___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_symbol___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_Syntax_getHeadInfo___main___spec__1___boxed(lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_LeanInit_9__decodeHexLitAux___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_numLitKind___closed__2;
|
||||
lean_object* l_Lean_ParserDescr_node(uint8_t, lean_object*, lean_object*);
|
||||
|
|
@ -272,6 +285,7 @@ lean_object* l_Lean_Syntax_getKind(lean_object*);
|
|||
lean_object* l_Lean_MacroScopesView_review(lean_object*);
|
||||
lean_object* l_Lean_Syntax_getArg___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Array_filterSepElems(lean_object*, lean_object*);
|
||||
lean_object* l_Array_mapSepElemsM___at_Array_mapSepElems___spec__1(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_identToAtom(lean_object*);
|
||||
lean_object* l_Lean_Name_Name_beq___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_getHeadInfo___boxed(lean_object*);
|
||||
|
|
@ -282,6 +296,7 @@ extern lean_object* l___private_Init_Util_1__mkPanicMessage___closed__2;
|
|||
lean_object* l___private_Init_LeanInit_7__decodeOctalLitAux___main(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_NameGenerator_curr(lean_object*);
|
||||
lean_object* l_Lean_Syntax_isTermId_x3f___boxed(lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_LeanInit_15__mapSepElemsMAux___main___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_isNameLit_x3f___boxed(lean_object*);
|
||||
lean_object* l___private_Init_LeanInit_12__decodeQuotedChar___boxed__const__2;
|
||||
lean_object* l_Lean_mkHole___closed__1;
|
||||
|
|
@ -326,11 +341,13 @@ lean_object* l_Lean_Macro_throwUnsupported(lean_object*, lean_object*);
|
|||
lean_object* lean_mk_syntax_ident(lean_object*);
|
||||
lean_object* l_Lean_mkStxLit(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_LeanInit_15__mapSepElemsMAux___main___at_Array_mapSepElems___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_toNat(lean_object*);
|
||||
lean_object* l___private_Init_LeanInit_14__filterSepElemsMAux___main(lean_object*);
|
||||
lean_object* l_Lean_mkOptionalNode___closed__2;
|
||||
lean_object* l_Lean_Syntax_getOptional_x3f___boxed(lean_object*);
|
||||
lean_object* l_Lean_mkCIdentFrom___closed__2;
|
||||
lean_object* lean_nat_mod(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Name_eraseMacroScopes___boxed(lean_object*);
|
||||
lean_object* l_Lean_mkCTermIdFrom(lean_object*, lean_object*);
|
||||
lean_object* l_Substring_takeWhileAux___main___at___private_Init_LeanInit_13__decodeNameLitAux___main___spec__2___boxed(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -371,6 +388,7 @@ lean_object* l___private_Init_LeanInit_14__filterSepElemsMAux___main___rarg(lean
|
|||
uint8_t l_Lean_isIdRest(uint32_t);
|
||||
lean_object* l_Lean_NameGenerator_Inhabited___closed__3;
|
||||
lean_object* l_Lean_Syntax_isIdent___boxed(lean_object*);
|
||||
lean_object* l___private_Init_LeanInit_15__mapSepElemsMAux___main___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_MacroM_monadQuotation___closed__4;
|
||||
lean_object* l_Lean_nameLitKind___closed__1;
|
||||
uint8_t lean_string_dec_eq(lean_object*, lean_object*);
|
||||
|
|
@ -2248,7 +2266,7 @@ lean_dec(x_1);
|
|||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findMAux___main___at_Lean_Syntax_getHeadInfo___main___spec__1(lean_object* x_1, lean_object* x_2) {
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_Syntax_getHeadInfo___main___spec__1(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3; uint8_t x_4;
|
||||
|
|
@ -2300,7 +2318,7 @@ case 1:
|
|||
lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_3 = lean_ctor_get(x_1, 1);
|
||||
x_4 = lean_unsigned_to_nat(0u);
|
||||
x_5 = l_Array_findMAux___main___at_Lean_Syntax_getHeadInfo___main___spec__1(x_3, x_4);
|
||||
x_5 = l_Array_findSomeMAux___main___at_Lean_Syntax_getHeadInfo___main___spec__1(x_3, x_4);
|
||||
return x_5;
|
||||
}
|
||||
default:
|
||||
|
|
@ -2313,11 +2331,11 @@ return x_6;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_findMAux___main___at_Lean_Syntax_getHeadInfo___main___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
lean_object* l_Array_findSomeMAux___main___at_Lean_Syntax_getHeadInfo___main___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l_Array_findMAux___main___at_Lean_Syntax_getHeadInfo___main___spec__1(x_1, x_2);
|
||||
x_3 = l_Array_findSomeMAux___main___at_Lean_Syntax_getHeadInfo___main___spec__1(x_1, x_2);
|
||||
lean_dec(x_1);
|
||||
return x_3;
|
||||
}
|
||||
|
|
@ -6498,6 +6516,250 @@ lean_dec(x_1);
|
|||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Init_LeanInit_15__mapSepElemsMAux___main___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
|
||||
x_7 = lean_unsigned_to_nat(1u);
|
||||
x_8 = lean_nat_add(x_1, x_7);
|
||||
x_9 = lean_array_push(x_2, x_6);
|
||||
x_10 = l___private_Init_LeanInit_15__mapSepElemsMAux___main___rarg(x_3, x_4, x_5, x_8, x_9);
|
||||
return x_10;
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Init_LeanInit_15__mapSepElemsMAux___main___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_6; uint8_t x_7;
|
||||
x_6 = lean_array_get_size(x_2);
|
||||
x_7 = lean_nat_dec_lt(x_4, x_6);
|
||||
lean_dec(x_6);
|
||||
if (x_7 == 0)
|
||||
{
|
||||
lean_object* x_8; lean_object* x_9; lean_object* x_10;
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
x_8 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_8);
|
||||
lean_dec(x_1);
|
||||
x_9 = lean_ctor_get(x_8, 1);
|
||||
lean_inc(x_9);
|
||||
lean_dec(x_8);
|
||||
x_10 = lean_apply_2(x_9, lean_box(0), x_5);
|
||||
return x_10;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; uint8_t x_15;
|
||||
x_11 = lean_array_fget(x_2, x_4);
|
||||
x_12 = lean_unsigned_to_nat(2u);
|
||||
x_13 = lean_nat_mod(x_4, x_12);
|
||||
x_14 = lean_unsigned_to_nat(0u);
|
||||
x_15 = lean_nat_dec_eq(x_13, x_14);
|
||||
lean_dec(x_13);
|
||||
if (x_15 == 0)
|
||||
{
|
||||
lean_object* x_16; lean_object* x_17; lean_object* x_18;
|
||||
x_16 = lean_unsigned_to_nat(1u);
|
||||
x_17 = lean_nat_add(x_4, x_16);
|
||||
lean_dec(x_4);
|
||||
x_18 = lean_array_push(x_5, x_11);
|
||||
x_4 = x_17;
|
||||
x_5 = x_18;
|
||||
goto _start;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23;
|
||||
x_20 = lean_ctor_get(x_1, 1);
|
||||
lean_inc(x_20);
|
||||
lean_inc(x_3);
|
||||
x_21 = lean_apply_1(x_3, x_11);
|
||||
x_22 = lean_alloc_closure((void*)(l___private_Init_LeanInit_15__mapSepElemsMAux___main___rarg___lambda__1___boxed), 6, 5);
|
||||
lean_closure_set(x_22, 0, x_4);
|
||||
lean_closure_set(x_22, 1, x_5);
|
||||
lean_closure_set(x_22, 2, x_1);
|
||||
lean_closure_set(x_22, 3, x_2);
|
||||
lean_closure_set(x_22, 4, x_3);
|
||||
x_23 = lean_apply_4(x_20, lean_box(0), lean_box(0), x_21, x_22);
|
||||
return x_23;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Init_LeanInit_15__mapSepElemsMAux___main(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = lean_alloc_closure((void*)(l___private_Init_LeanInit_15__mapSepElemsMAux___main___rarg), 5, 0);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Init_LeanInit_15__mapSepElemsMAux___main___rarg___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_7;
|
||||
x_7 = l___private_Init_LeanInit_15__mapSepElemsMAux___main___rarg___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6);
|
||||
lean_dec(x_1);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Init_LeanInit_15__mapSepElemsMAux___main___boxed(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = l___private_Init_LeanInit_15__mapSepElemsMAux___main(x_1);
|
||||
lean_dec(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Init_LeanInit_15__mapSepElemsMAux___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_6;
|
||||
x_6 = l___private_Init_LeanInit_15__mapSepElemsMAux___main___rarg(x_1, x_2, x_3, x_4, x_5);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Init_LeanInit_15__mapSepElemsMAux(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = lean_alloc_closure((void*)(l___private_Init_LeanInit_15__mapSepElemsMAux___rarg), 5, 0);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Init_LeanInit_15__mapSepElemsMAux___boxed(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = l___private_Init_LeanInit_15__mapSepElemsMAux(x_1);
|
||||
lean_dec(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_mapSepElemsM___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4; lean_object* x_5; lean_object* x_6;
|
||||
x_4 = lean_unsigned_to_nat(0u);
|
||||
x_5 = l_Array_empty___closed__1;
|
||||
x_6 = l___private_Init_LeanInit_15__mapSepElemsMAux___main___rarg(x_1, x_2, x_3, x_4, x_5);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_mapSepElemsM(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = lean_alloc_closure((void*)(l_Array_mapSepElemsM___rarg), 3, 0);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_mapSepElemsM___boxed(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = l_Array_mapSepElemsM(x_1);
|
||||
lean_dec(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Init_LeanInit_15__mapSepElemsMAux___main___at_Array_mapSepElems___spec__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5; uint8_t x_6;
|
||||
x_5 = lean_array_get_size(x_1);
|
||||
x_6 = lean_nat_dec_lt(x_3, x_5);
|
||||
lean_dec(x_5);
|
||||
if (x_6 == 0)
|
||||
{
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
return x_4;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11;
|
||||
x_7 = lean_array_fget(x_1, x_3);
|
||||
x_8 = lean_unsigned_to_nat(2u);
|
||||
x_9 = lean_nat_mod(x_3, x_8);
|
||||
x_10 = lean_unsigned_to_nat(0u);
|
||||
x_11 = lean_nat_dec_eq(x_9, x_10);
|
||||
lean_dec(x_9);
|
||||
if (x_11 == 0)
|
||||
{
|
||||
lean_object* x_12; lean_object* x_13; lean_object* x_14;
|
||||
x_12 = lean_unsigned_to_nat(1u);
|
||||
x_13 = lean_nat_add(x_3, x_12);
|
||||
lean_dec(x_3);
|
||||
x_14 = lean_array_push(x_4, x_7);
|
||||
x_3 = x_13;
|
||||
x_4 = x_14;
|
||||
goto _start;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
|
||||
lean_inc(x_2);
|
||||
x_16 = lean_apply_1(x_2, x_7);
|
||||
x_17 = lean_unsigned_to_nat(1u);
|
||||
x_18 = lean_nat_add(x_3, x_17);
|
||||
lean_dec(x_3);
|
||||
x_19 = lean_array_push(x_4, x_16);
|
||||
x_3 = x_18;
|
||||
x_4 = x_19;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_mapSepElemsM___at_Array_mapSepElems___spec__1(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_3 = lean_unsigned_to_nat(0u);
|
||||
x_4 = l_Array_empty___closed__1;
|
||||
x_5 = l___private_Init_LeanInit_15__mapSepElemsMAux___main___at_Array_mapSepElems___spec__2(x_1, x_2, x_3, x_4);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_mapSepElems(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l_Array_mapSepElemsM___at_Array_mapSepElems___spec__1(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Init_LeanInit_15__mapSepElemsMAux___main___at_Array_mapSepElems___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5;
|
||||
x_5 = l___private_Init_LeanInit_15__mapSepElemsMAux___main___at_Array_mapSepElems___spec__2(x_1, x_2, x_3, x_4);
|
||||
lean_dec(x_1);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_mapSepElemsM___at_Array_mapSepElems___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l_Array_mapSepElemsM___at_Array_mapSepElems___spec__1(x_1, x_2);
|
||||
lean_dec(x_1);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_mapSepElems___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l_Array_mapSepElems(x_1, x_2);
|
||||
lean_dec(x_1);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* initialize_Init_Data_String_Basic(lean_object*);
|
||||
lean_object* initialize_Init_Data_Array_Basic(lean_object*);
|
||||
lean_object* initialize_Init_Data_UInt(lean_object*);
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue