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

feat(library/init/lean/localcontext): add LocalContext.mkLambda and LocalContext.mkForall

Browse source
This commit is contained in:
Leonardo de Moura 2019-09-17 13:41:42 -07:00
parent eebc722f57
commit 06bb3a82d3
1 changed files with 23 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
library/init/lean/localcontext.lean
View file

@ -234,5 +234,28 @@ partial def isSubPrefixOfAux (a₁ a₂ : PArray (Option LocalDecl)) : Nat → N
def isSubPrefixOf (lctx₁ lctx₂ : LocalContext) : Bool :=
isSubPrefixOfAux lctx₁.decls lctx₂.decls 0 0
@[inline] def mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (b : Expr) : Expr :=
let b := b.abstract xs;
xs.size.foldRev (fun i b =>
let x := xs.get i;
match lctx.findFVar x with
| some (LocalDecl.cdecl _ _ n ty bi) =>
let ty := ty.abstractRange i xs;
if isLambda then
Expr.lam n bi ty b
else
Expr.pi n bi ty b
| some (LocalDecl.ldecl _ _ n ty val) =>
let ty := ty.abstractRange i xs;
let val := val.abstractRange i xs;
Expr.elet n ty val b
| none => b) b
def mkLambda (lctx : LocalContext) (xs : Array Expr) (b : Expr) : Expr :=
mkBinding true lctx xs b
def mkForall (lctx : LocalContext) (xs : Array Expr) (b : Expr) : Expr :=
mkBinding false lctx xs b
end LocalContext
end Lean