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

fix: reducibility setting should not hide non-definitions (constructors, inductive types, etc)

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-23 09:36:22 -08:00
parent 4a6d0a8082
commit 63d3429246
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -314,10 +314,11 @@ do env ← getEnv;
match env.find constName with
| some (info@(ConstantInfo.thmInfo _)) =>
condM reduceAll? (pure (some info)) (pure none)
| some info =>
| some (info@(ConstantInfo.defnInfo _)) =>
condM reduceReducibleOnly?
(condM (isReducible constName) (pure (some info)) (pure none))
(pure (some info))
| some info => pure (some info)
| none =>
if exception? then throwEx $ Exception.unknownConst constName
else pure none