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

chore: remove ParamInfo.proof field

Browse source 
It is an approximation because of dependent types.
Moreover, the new `isProofQuick` should make `isProof` much cheaper.
This commit is contained in:
Leonardo de Moura 2019-11-25 08:33:30 -08:00
parent ec0eed582e
commit 292603f8bb
2 changed files with 0 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Init/Lean/Meta/Basic.lean
View file

@ -82,7 +82,6 @@ structure Config :=
structure ParamInfo :=
(implicit : Bool := false)
(instImplicit : Bool := false)
(proof : Bool := false)
(hasFwdDeps : Bool := false)
(backDeps : Array Nat := #[])

2
src/Init/Lean/Meta/FunInfo.lean
View file

@ -62,12 +62,10 @@ checkFunInfoCache fn maxArgs? $ do
(fun (i : Nat) (pinfo : Array ParamInfo) => do
let fvar := fvars.get! i;
decl ← getFVarLocalDecl fvar;
proof ← isProp decl.type;
let backDeps := collectDeps fvars decl.type;
let pinfo := updateHasFwdDeps pinfo backDeps;
pure $ pinfo.push {
backDeps := backDeps,
proof := proof,
implicit := decl.binderInfo == BinderInfo.implicit,
instImplicit := decl.binderInfo == BinderInfo.instImplicit })
#[];