Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+โ†‘Ctrl+โ†“to navigate, Ctrl+๐Ÿ–ฑ๏ธto focus. On Mac, use Cmdinstead of Ctrl. 
/-
Copyright (c) 2022 Siddhartha Gadgil. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gabriel Ebner, Siddhartha Gadgil, Jannis Limperg
-/
import Lean
import Std.Tactic.RCases
import Mathlib.Tactic.Cache

open Lean (HashSet)
open Lean Meta Elab Tactic

namespace Mathlib.Tactic

/--
Get all metavariables which `mvarId` depends on. These are the metavariables
which occur in the target or local context or delayed assignment (if any) of
`mvarId`, plus the metvariables which occur in these metavariables, etc.
-/
partial def 
getUnassignedGoalMVarDependencies: MVarId โ†’ MetaM (HashSet MVarId)
getUnassignedGoalMVarDependencies (
mvarId: MVarId
mvarId : 
MVarId: Type
MVarId) :
    
MetaM: Type โ†’ Type
MetaM (
HashSet: (ฮฑ : Type ?u.4) โ†’ [inst : BEq ฮฑ] โ†’ [inst : Hashable ฮฑ] โ†’ Type ?u.4
HashSet 
MVarId: Type
MVarId) :=
  return 
(โ† go mvarId |>.run {}): ?m.3822
(โ† 
go: MVarId โ†’ StateRefT' IO.RealWorld (HashSet MVarId) MetaM Unit
go
(โ† go mvarId |>.run {}): ?m.3822
 
mvarId: MVarId
mvarId
(โ† go mvarId |>.run {}): ?m.3822
 |>.
run: {ฯ‰ ฯƒ : Type} โ†’
  {m : Type โ†’ Type} โ†’ [inst : Monad m] โ†’ [inst : MonadLiftT (ST ฯ‰) m] โ†’ {ฮฑ : Type} โ†’ StateRefT' ฯ‰ ฯƒ m ฮฑ โ†’ ฯƒ โ†’ m (ฮฑ ร— ฯƒ)
run
(โ† go mvarId |>.run {}): ?m.3822
 
{}: ?m.3763
{}
(โ† go mvarId |>.run {}): ?m.3822
).
snd: {ฮฑ : Type ?u.3850} โ†’ {ฮฒ : Type ?u.3849} โ†’ ฮฑ ร— ฮฒ โ†’ ฮฒ
snd
  where
    /-- auxiliary function for `getUnassignedGoalMVarDependencies` -/
    
addMVars: Expr โ†’ StateRefT' IO.RealWorld (HashSet MVarId) MetaM Unit
addMVars (
e: Expr
e : 
Expr: Type
Expr) : StateRefT (
HashSet: (ฮฑ : Type ?u.19) โ†’ [inst : BEq ฮฑ] โ†’ [inst : Hashable ฮฑ] โ†’ Type ?u.19
HashSet 
MVarId: Type
MVarId) 
MetaM: Type โ†’ Type
MetaM 
Unit: Type
Unit := do
      let 
mvars: ?m.337
mvars โ† 
getMVars: Expr โ†’ MetaM (Array MVarId)
getMVars 
e: Expr
e
      let mut 
s: ?m.594
s โ† 
get: {ฯƒ : outParam (Type ?u.376)} โ†’ {m : Type ?u.376 โ†’ Type ?u.375} โ†’ [self : MonadState ฯƒ m] โ†’ m ฯƒ
get
      
set: {ฯƒ : semiOutParam (Type ?u.633)} โ†’ {m : Type ?u.633 โ†’ Type ?u.632} โ†’ [self : MonadStateOf ฯƒ m] โ†’ ฯƒ โ†’ m PUnit
set (
{}: ?m.658
{} : 
HashSet: (ฮฑ : Type ?u.654) โ†’ [inst : BEq ฮฑ] โ†’ [inst : Hashable ฮฑ] โ†’ Type ?u.654
HashSet 
MVarId: Type
MVarId) -- Ensure that `s` is not shared.
      for 
mvarId: ?m.976
mvarId in 
mvars: ?m.337
mvars do
        unless โ† 
mvarId: ?m.976
mvarId.
isDelayedAssigned: {m : Type โ†’ Type} โ†’ [inst : Monad m] โ†’ [inst : MonadMCtx m] โ†’ MVarId โ†’ m Bool
isDelayedAssigned do
          
s: ?m.982
s := 
s: ?m.982
s.
insert: {ฮฑ : Type ?u.1301} โ†’ {x : BEq ฮฑ} โ†’ {x_1 : Hashable ฮฑ} โ†’ HashSet ฮฑ โ†’ ฮฑ โ†’ HashSet ฮฑ
insert 
mvarId: ?m.976
mvarId
      
set: {ฯƒ : semiOutParam (Type ?u.1491)} โ†’ {m : Type ?u.1491 โ†’ Type ?u.1490} โ†’ [self : MonadStateOf ฯƒ m] โ†’ ฯƒ โ†’ m PUnit
set 
s: ?m.1452
s
      
mvars: ?m.337
mvars.
forM: {ฮฑ : Type ?u.1522} โ†’
  {m : Type ?u.1521 โ†’ Type ?u.1520} โ†’
    [inst : Monad m] โ†’ (ฮฑ โ†’ m PUnit) โ†’ (as : Array ฮฑ) โ†’ optParam โ„• 0 โ†’ optParam โ„• (Array.size as) โ†’ m PUnit
forM 
go: MVarId โ†’ StateRefT' IO.RealWorld (HashSet MVarId) MetaM Unit
go
    /-- auxiliary function for `getUnassignedGoalMVarDependencies` -/
    
go: MVarId โ†’ StateRefT' IO.RealWorld (HashSet MVarId) MetaM Unit
go (
mvarId: MVarId
mvarId : 
MVarId: Type
MVarId) : StateRefT (
HashSet: (ฮฑ : Type ?u.110) โ†’ [inst : BEq ฮฑ] โ†’ [inst : Hashable ฮฑ] โ†’ Type ?u.110
HashSet 
MVarId: Type
MVarId) 
MetaM: Type โ†’ Type
MetaM 
Unit: Type
Unit :=
      
withIncRecDepth: {m : Type โ†’ Type} โ†’ {ฮฑ : Type} โ†’ [inst : Monad m] โ†’ [inst : MonadError m] โ†’ [inst : MonadRecDepth m] โ†’ m ฮฑ โ†’ m ฮฑ
withIncRecDepth do
        let 
mdecl: ?m.1743
mdecl โ† 
mvarId: MVarId
mvarId.
getDecl: MVarId โ†’ MetaM MetavarDecl
getDecl
        
addMVars: Expr โ†’ StateRefT' IO.RealWorld (HashSet MVarId) MetaM Unit
addMVars 
mdecl: ?m.1743
mdecl.
type: MetavarDecl โ†’ Expr
type
        for 
ldecl: ?m.1879
ldecl in 
mdecl: ?m.1743
mdecl.
lctx: MetavarDecl โ†’ LocalContext
lctx do
          
addMVars: Expr โ†’ StateRefT' IO.RealWorld (HashSet MVarId) MetaM Unit
addMVars 
ldecl: ?m.1879
ldecl.
type: LocalDecl โ†’ Expr
type
          if let (
some: {ฮฑ : Type ?u.1938} โ†’ ฮฑ โ†’ Option ฮฑ
some 
val: Expr
val) := 
ldecl: ?m.1879
ldecl.
value?: LocalDecl โ†’ Option Expr
value? then
            
addMVars: Expr โ†’ StateRefT' IO.RealWorld (HashSet MVarId) MetaM Unit
addMVars 
val: Expr
val
        if let (
some: {ฮฑ : Type ?u.2386} โ†’ ฮฑ โ†’ Option ฮฑ
some 
ass: DelayedMetavarAssignment
ass) โ† 
getDelayedMVarAssignment?: {m : Type โ†’ Type} โ†’ [inst : Monad m] โ†’ [inst : MonadMCtx m] โ†’ MVarId โ†’ m (Option DelayedMetavarAssignment)
getDelayedMVarAssignment? 
mvarId: MVarId
mvarId then
          let 
pendingMVarId: ?m.2402
pendingMVarId := 
ass: DelayedMetavarAssignment
ass.
mvarIdPending: DelayedMetavarAssignment โ†’ MVarId
mvarIdPending
          unless โ† 
pendingMVarId: ?m.2402
pendingMVarId.
isAssigned: {m : Type โ†’ Type} โ†’ [inst : Monad m] โ†’ [inst : MonadMCtx m] โ†’ MVarId โ†’ m Bool
isAssigned <||> 
pendingMVarId: ?m.2402
pendingMVarId.
isDelayedAssigned: {m : Type โ†’ Type} โ†’ [inst : Monad m] โ†’ [inst : MonadMCtx m] โ†’ MVarId โ†’ m Bool
isDelayedAssigned do
            
modify: {ฯƒ : Type ?u.2792} โ†’ {m : Type ?u.2792 โ†’ Type ?u.2791} โ†’ [inst : MonadState ฯƒ m] โ†’ (ฯƒ โ†’ ฯƒ) โ†’ m PUnit
modify
modify (ยท.insert pendingMVarId): StateRefT' IO.RealWorld (HashSet MVarId) MetaM (?m.2539 yโœ)
 (ยท.
insert: {ฮฑ : Type ?u.3138} โ†’ {x : BEq ฮฑ} โ†’ {x_1 : Hashable ฮฑ} โ†’ HashSet ฮฑ โ†’ ฮฑ โ†’ HashSet ฮฑ
insert
modify (ยท.insert pendingMVarId): StateRefT' IO.RealWorld (HashSet MVarId) MetaM (?m.2539 yโœ)
 
pendingMVarId: ?m.2402
pendingMVarId
modify (ยท.insert pendingMVarId): StateRefT' IO.RealWorld (HashSet MVarId) MetaM (?m.2539 yโœ)
)
          
go: MVarId โ†’ StateRefT' IO.RealWorld (HashSet MVarId) MetaM Unit
go 
pendingMVarId: ?m.2402
pendingMVarId

/-- Modifier `recover` for a tactic (sequence) to debug cases where goals are closed incorrectly.
The tactic `recover tacs` for a tactic (sequence) tacs applies the tactics and then adds goals
that are not closed starting from the original -/
elab "recover" 
tacs: ?m.17840
tacs:
tacticSeq: Parser.Parser
tacticSeq : 
tactic: Parser.Category
tactic => do
  let 
originalGoals: ?m.17917
originalGoals โ† 
getGoals: TacticM (List MVarId)
getGoals
  
evalTactic: Syntax โ†’ TacticM Unit
evalTactic 
tacs: ?m.17840
tacs
  let mut 
unassigned: HashSet MVarId
unassigned : 
HashSet: (ฮฑ : Type ?u.18085) โ†’ [inst : BEq ฮฑ] โ†’ [inst : Hashable ฮฑ] โ†’ Type ?u.18085
HashSet 
MVarId: Type
MVarId := 
{}: ?m.18094
{}
  for 
mvarId: ?m.18238
mvarId in 
originalGoals: ?m.17917
originalGoals do
    unless โ† 
mvarId: ?m.18238
mvarId.
isAssigned: {m : Type โ†’ Type} โ†’ [inst : Monad m] โ†’ [inst : MonadMCtx m] โ†’ MVarId โ†’ m Bool
isAssigned <||> 
mvarId: ?m.18238
mvarId.
isDelayedAssigned: {m : Type โ†’ Type} โ†’ [inst : Monad m] โ†’ [inst : MonadMCtx m] โ†’ MVarId โ†’ m Bool
isDelayedAssigned do
      
unassigned: ?m.18244
unassigned := 
unassigned: ?m.18244
unassigned.
insert: {ฮฑ : Type ?u.18677} โ†’ {x : BEq ฮฑ} โ†’ {x_1 : Hashable ฮฑ} โ†’ HashSet ฮฑ โ†’ ฮฑ โ†’ HashSet ฮฑ
insert 
mvarId: ?m.18238
mvarId
    let 
unassignedMVarDependencies: ?m.19002
unassignedMVarDependencies โ† 
getUnassignedGoalMVarDependencies: MVarId โ†’ MetaM (HashSet MVarId)
getUnassignedGoalMVarDependencies 
mvarId: ?m.18238
mvarId
    
unassigned: HashSet MVarId
unassigned := 
unassigned: HashSet MVarId
unassigned.
insertMany: {ฮฑ : Type ?u.19007} โ†’
  {x : BEq ฮฑ} โ†’ {x_1 : Hashable ฮฑ} โ†’ {ฯ : Type ?u.19006} โ†’ [inst : ForIn Id ฯ ฮฑ] โ†’ HashSet ฮฑ โ†’ ฯ โ†’ HashSet ฮฑ
insertMany 
unassignedMVarDependencies: ?m.19002
unassignedMVarDependencies.
toList: {ฮฑ : Type ?u.19124} โ†’ {x : BEq ฮฑ} โ†’ {x_1 : Hashable ฮฑ} โ†’ HashSet ฮฑ โ†’ List ฮฑ
toList
  
setGoals: List MVarId โ†’ TacticM Unit
setGoals <| ((โ† 
getGoals: TacticM (List MVarId)
getGoals) ++ 
unassigned: ?m.19322
unassigned.
toList: {ฮฑ : Type ?u.19384} โ†’ {x : BEq ฮฑ} โ†’ {x_1 : Hashable ฮฑ} โ†’ HashSet ฮฑ โ†’ List ฮฑ
toList).
eraseDups: {ฮฑ : Type ?u.19427} โ†’ [inst : BEq ฮฑ] โ†’ List ฮฑ โ†’ List ฮฑ
eraseDups