/-
Copyright (c) 2022 Jannis Limperg. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jannis Limperg
-/

import Std.Lean.Meta.Basic

open Lean Lean.Meta

/--
Try to clear the given fvars from the local context. Returns the new goal and
the hypotheses that were cleared. Unlike `Lean.MVarId.tryClearMany`, this
function does not require the `hyps` to be given in the order in which they
appear in the local context.
-/
def 
Lean.MVarId.tryClearMany': MVarId → Array FVarId → MetaM (MVarId × Array FVarId)
Lean.MVarId.tryClearMany' (
goal: MVarId
goal : 
MVarId: Type
MVarId) (
hyps: Array FVarId
hyps : 
Array: Type ?u.4 → Type ?u.4
Array 
FVarId: Type
FVarId) :
    
MetaM: Type → Type
MetaM (
MVarId: Type
MVarId × 
Array: Type ?u.9 → Type ?u.9
Array 
FVarId: Type
FVarId) :=
  
goal: MVarId
goal.
withContext: {n : Type → Type ?u.15} → [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → MVarId → n α → n α
withContext do
    let 
hyps: ?m.153
hyps ← 
sortFVarsByContextOrder: {m : Type → Type} → [inst : Monad m] → [inst : MonadLCtx m] → Array FVarId → m (Array FVarId)
sortFVarsByContextOrder 
hyps: Array FVarId
hyps
    
hyps: ?m.153
hyps.
foldrM: {α : Type ?u.157} →
  {β : Type ?u.156} →
    {m : Type ?u.156 → Type ?u.155} →
      [inst : Monad m] → (α → β → m β) → β → (as : Array α) → optParam Nat (Array.size as) → optParam Nat 0 → m β
foldrM (init := (
goal: MVarId
goal, 
Array.mkEmpty: {α : Type ?u.547} → Nat → Array α
Array.mkEmpty 
hyps: ?m.153
hyps.
size: {α : Type ?u.550} → Array α → Nat
size))
      λ 
h: ?m.198
h (
goal: MVarId
goal, 
cleared: Array FVarId
cleared) => do
        let 
goal': ?m.288
goal' ← 
goal: MVarId
goal.
tryClear: MVarId → FVarId → MetaM MVarId
tryClear 
h: ?m.198
h
        let 
cleared: ?m.291
cleared := if 
goal: MVarId
goal == 
goal': ?m.288
goal' then 
cleared: Array FVarId
cleared else 
cleared: Array FVarId
cleared.
push: {α : Type ?u.388} → Array α → α → Array α
push 
h: ?m.198
h
        return (
goal': ?m.288
goal', 
cleared: ?m.291
cleared)