chore: naming convention

suffix `?` should only be used for functions/methods returning `Bool`.
This commit is contained in:
Leonardo de Moura 2019-11-27 05:50:31 -08:00
parent dfbc9cb8b5
commit e99f8a9d22
2 changed files with 5 additions and 5 deletions

View file

@ -231,10 +231,10 @@ throwEx $ Exception.bug b
do ctx ← read;
when ctx.config.debug (do x; pure ())
@[inline] def reduceAll? : MetaM Bool :=
@[inline] def shouldReduceAll : MetaM Bool :=
do ctx ← read; pure $ ctx.config.transparency == TransparencyMode.all
@[inline] def reduceReducibleOnly? : MetaM Bool :=
@[inline] def shouldReduceReducibleOnly : MetaM Bool :=
do ctx ← read; pure $ ctx.config.transparency == TransparencyMode.reducible
@[inline] def getTransparency : MetaM TransparencyMode :=
@ -312,9 +312,9 @@ def getConstAux (constName : Name) (exception? : Bool) : MetaM (Option ConstantI
do env ← getEnv;
match env.find constName with
| some (info@(ConstantInfo.thmInfo _)) =>
condM reduceAll? (pure (some info)) (pure none)
condM shouldReduceAll (pure (some info)) (pure none)
| some (info@(ConstantInfo.defnInfo _)) =>
condM reduceReducibleOnly?
condM shouldReduceReducibleOnly
(condM (isReducible constName) (pure (some info)) (pure none))
(pure (some info))
| some info => pure (some info)

View file

@ -805,7 +805,7 @@ else
Auxiliary method for isDefEqDelta -/
private def unfoldReducibeDefEq (tInfo sInfo : ConstantInfo) (t s : Expr) : MetaM LBool :=
condM reduceReducibleOnly?
condM shouldReduceReducibleOnly
(unfoldDefEq tInfo sInfo t s)
(do tReducible ← isReducible tInfo.name;
sReducible ← isReducible sInfo.name;