/-
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

namespace Lean.Meta

/--
Description of a hypothesis for `Lean.MVarId.assertHypotheses'`.
-/
structure 
Hypothesis': Type
Hypothesis' extends 
Hypothesis: Type
Hypothesis where
  /-- The hypothesis' `BinderInfo` -/
  
binderInfo: Hypothesis' → BinderInfo
binderInfo : 
BinderInfo: Type
BinderInfo
  /-- The hypothesis' `LocalDeclKind` -/
  
kind: Hypothesis' → LocalDeclKind
kind : 
LocalDeclKind: Type
LocalDeclKind

/--
Add the given hypotheses to the local context. This is a generalisation of
`Lean.MVarId.assertHypotheses` which lets you specify
-/
def 
_root_.Lean.MVarId.assertHypotheses': MVarId → Array Hypothesis' → MetaM (Array FVarId × MVarId)
_root_.Lean.MVarId.assertHypotheses' (
mvarId: MVarId
mvarId : 
MVarId: Type
MVarId)
    (
hs: Array Hypothesis'
hs : 
Array: Type ?u.454 → Type ?u.454
Array 
Hypothesis': Type
Hypothesis') : 
MetaM: Type → Type
MetaM (
Array: Type ?u.459 → Type ?u.459
Array 
FVarId: Type
FVarId × 
MVarId: Type
MVarId) := do
  let (
fvarIds: Array FVarId
fvarIds, 
mvarId: MVarId
mvarId) ← 
mvarId: MVarId
mvarId.
assertHypotheses: MVarId → Array Hypothesis → MetaM (Array FVarId × MVarId)
assertHypotheses $ 
hs: Array Hypothesis'
hs.
map: {α : Type ?u.540} → {β : Type ?u.539} → (α → β) → Array α → Array β
map (·.
toHypothesis: Hypothesis' → Hypothesis
toHypothesis)
  
mvarId: MVarId
mvarId.
modifyLCtx: {m : Type → Type} → [inst : MonadMCtx m] → MVarId → (LocalContext → LocalContext) → m Unit
modifyLCtx λ 
lctx: ?m.635
lctx => 
Id.run: {α : Type ?u.637} → Id α → α
Id.run do
    let mut 
lctx: ?m.757
lctx := 
lctx: ?m.635
lctx
    for 
h: ?m.751
h : 
i: ?m.748
i in [:
hs: Array Hypothesis'
hs.
size: {α : Type ?u.694} → Array α → Nat
size] do
      let 
h: ?m.760
h := 
hs: Array Hypothesis'
hs[
i: ?m.748
i]'
h: ?m.751
h.
2: ∀ {a b : Prop}, a ∧ b → b
2
      if 
h: ?m.760
h.
kind: Hypothesis' → LocalDeclKind
kind != 
.default: LocalDeclKind
.default then
        
lctx: LocalContext
lctx := 
lctx: ?m.757
lctx.
setKind: LocalContext → FVarId → LocalDeclKind → LocalContext
setKind 
fvarIds: Array FVarId
fvarIds[
i: ?m.748
i]! 
h: ?m.760
h.
kind: Hypothesis' → LocalDeclKind
kind
      if 
h: ?m.760
h.
binderInfo: Hypothesis' → BinderInfo
binderInfo != 
.default: BinderInfo
.default then
        
lctx: ?m.1265
lctx := 
lctx: LocalContext
lctx.
setBinderInfo: LocalContext → FVarId → BinderInfo → LocalContext
setBinderInfo 
fvarIds: Array FVarId
fvarIds[
i: ?m.748
i]! 
h: ?m.760
h.
binderInfo: Hypothesis' → BinderInfo
binderInfo
    
pure: {f : Type ?u.1529 → Type ?u.1528} → [self : Pure f] → {α : Type ?u.1529} → α → f α
pure 
lctx: ?m.1526
lctx
  return (
fvarIds: Array FVarId
fvarIds, 
mvarId: MVarId
mvarId)

end Lean.Meta