max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2021-12-02 15:02:57 -08:00
parent c7565c446a
commit 01615f175c
1 changed files with 10 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

33
src/Lean/LocalContext.lean
View file

@ -257,27 +257,22 @@ def numIndices (lctx : LocalContext) : Nat :=
def getAt? (lctx : LocalContext) (i : Nat) : Option LocalDecl :=
lctx.decls.get! i
section
universe u v
variable {m : Type u → Type v} [Monad m]
variable {β : Type u}
@[specialize] def foldlM (lctx : LocalContext) (f : β → LocalDecl → m β) (init : β) (start : Nat := 0) : m β :=
@[specialize] def foldlM [Monad m] (lctx : LocalContext) (f : β → LocalDecl → m β) (init : β) (start : Nat := 0) : m β :=
lctx.decls.foldlM (init := init) (start := start) fun b decl => match decl with
| none => pure b
| some decl => f b decl
@[specialize] def forM (lctx : LocalContext) (f : LocalDecl → m PUnit) : m PUnit :=
@[specialize] def forM [Monad m] (lctx : LocalContext) (f : LocalDecl → m PUnit) : m PUnit :=
lctx.decls.forM fun decl => match decl with
| none => pure PUnit.unit
| some decl => f decl
@[specialize] def findDeclM? (lctx : LocalContext) (f : LocalDecl → m (Option β)) : m (Option β) :=
@[specialize] def findDeclM? [Monad m] (lctx : LocalContext) (f : LocalDecl → m (Option β)) : m (Option β) :=
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 β) :=
@[specialize] def findDeclRevM? [Monad m] (lctx : LocalContext) (f : LocalDecl → m (Option β)) : m (Option β) :=
lctx.decls.findSomeRevM? fun decl => match decl with
| none => pure none
| some decl => f decl
@ -287,15 +282,13 @@ instance : ForIn m LocalContext LocalDecl where
| none => ForInStep.yield b
| some d => f d b
end
@[inline] def foldl {β} (lctx : LocalContext) (f : β → LocalDecl → β) (init : β) (start : Nat := 0) : β :=
@[inline] def foldl (lctx : LocalContext) (f : β → LocalDecl → β) (init : β) (start : Nat := 0) : β :=
Id.run <| lctx.foldlM f init start
@[inline] def findDecl? {β} (lctx : LocalContext) (f : LocalDecl → Option β) : Option β :=
@[inline] def findDecl? (lctx : LocalContext) (f : LocalDecl → Option β) : Option β :=
Id.run <| lctx.findDeclM? f
@[inline] def findDeclRev? {β} (lctx : LocalContext) (f : LocalDecl → Option β) : Option β :=
@[inline] def findDeclRev? (lctx : LocalContext) (f : LocalDecl → Option β) : Option β :=
Id.run <| lctx.findDeclRevM? f
partial def isSubPrefixOfAux (a₁ a₂ : PArray (Option LocalDecl)) (exceptFVars : Array Expr) (i j : Nat) : Bool :=
@ -344,22 +337,16 @@ def mkLambda (lctx : LocalContext) (xs : Array Expr) (b : Expr) : Expr :=
def mkForall (lctx : LocalContext) (xs : Array Expr) (b : Expr) : Expr :=
mkBinding false lctx xs b
section
universe u
variable {m : Type → Type u} [Monad m]
@[inline] def anyM (lctx : LocalContext) (p : LocalDecl → m Bool) : m Bool :=
@[inline] def anyM [Monad m] (lctx : LocalContext) (p : LocalDecl → m Bool) : m Bool :=
lctx.decls.anyM fun d => match d with
| some decl => p decl
| none => pure false
@[inline] def allM (lctx : LocalContext) (p : LocalDecl → m Bool) : m Bool :=
@[inline] def allM [Monad m] (lctx : LocalContext) (p : LocalDecl → m Bool) : m Bool :=
lctx.decls.allM fun d => match d with
| some decl => p decl
| none => pure true
end
@[inline] def any (lctx : LocalContext) (p : LocalDecl → Bool) : Bool :=
Id.run <| lctx.anyM p
@ -389,7 +376,7 @@ class MonadLCtx (m : Type → Type) where
export MonadLCtx (getLCtx)
instance (m n) [MonadLift m n] [MonadLCtx m] : MonadLCtx n where
instance [MonadLift m n] [MonadLCtx m] : MonadLCtx n where
getLCtx := liftM (getLCtx : m _)
def replaceFVarIdAtLocalDecl (fvarId : FVarId) (e : Expr) (d : LocalDecl) : LocalDecl :=