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

chore: use isProof

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-25 08:31:42 -08:00
parent 120778585d
commit ec0eed582e
1 changed files with 8 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/Init/Lean/Meta/DiscrTree.lean
View file

@ -6,6 +6,7 @@ Authors: Leonardo de Moura
prelude
import Init.Lean.Meta.Basic
import Init.Lean.Meta.FunInfo
import Init.Lean.Meta.InferType
namespace Lean
namespace Meta
@ -133,12 +134,14 @@ private partial def pushArgsAux (infos : Array ParamInfo) : Nat → Expr → Arr
| i, Expr.app f a _, todo =>
if h : i < infos.size then
let info := infos.get ⟨i, h⟩;
if info.implicit || info.instImplicit || info.proof then
if info.implicit || info.instImplicit then
pushArgsAux (i-1) f (todo.push tmpStar)
else
pushArgsAux (i-1) f (todo.push a)
else
pushArgsAux (i-1) f (todo.push a)
else condM (isProof a)
(pushArgsAux (i-1) f (todo.push tmpStar))
(pushArgsAux (i-1) f (todo.push a))
else condM (isProof a)
(pushArgsAux (i-1) f (todo.push tmpStar))
(pushArgsAux (i-1) f (todo.push a))
| _, _, todo => pure todo
private def pushArgs (todo : Array Expr) (e : Expr) : MetaM (Key × Array Expr) :=