chore: valueOpt ==> value?

This commit is contained in:
Leonardo de Moura 2019-11-14 09:52:16 -08:00
parent 79c0833d06
commit 83e2796e96
2 changed files with 2 additions and 2 deletions

View file

@ -41,7 +41,7 @@ def binderInfo : LocalDecl → BinderInfo
| cdecl _ _ _ _ bi => bi
| ldecl _ _ _ _ _ => BinderInfo.default
def valueOpt : LocalDecl → Option Expr
def value? : LocalDecl → Option Expr
| cdecl _ _ _ _ _ => none
| ldecl _ _ _ _ v => some v

View file

@ -224,7 +224,7 @@ match rec.kind with
| e@(Expr.letE _ _ _ _), k => k e
| e@(Expr.fvar fvarId), k => do
decl ← getLocalDecl fvarId;
match decl.valueOpt with
match decl.value? with
| none => pure e
| some v => whnfEasyCases v k
| e@(Expr.mvar mvarId), k => do