From 83e2796e96e36cd5352b75969d7ea1a3e40d6291 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 14 Nov 2019 09:52:16 -0800 Subject: [PATCH] chore: `valueOpt` ==> `value?` --- library/Init/Lean/LocalContext.lean | 2 +- library/Init/Lean/WHNF.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/library/Init/Lean/LocalContext.lean b/library/Init/Lean/LocalContext.lean index d0674731f1..2f448cd1eb 100644 --- a/library/Init/Lean/LocalContext.lean +++ b/library/Init/Lean/LocalContext.lean @@ -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 diff --git a/library/Init/Lean/WHNF.lean b/library/Init/Lean/WHNF.lean index 28bce8c041..cfa45d4a9f 100644 --- a/library/Init/Lean/WHNF.lean +++ b/library/Init/Lean/WHNF.lean @@ -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