idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 11:05:17 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #1655 from edwinb/proofsearch-fix

Browse Source 
Don't inline holes that are user defined names
This commit is contained in:
Edwin Brady 2021-07-03 12:23:19 +01:00 committed by GitHub
commit 4fdec0682e
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 3 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/Core/Unify.idr
View File

@ -475,7 +475,9 @@ instantiate {newvars} loc mode env mname mref num mdef locs otm tm
rhs <- mkDef locs INil tm ty
logTerm "unify.instantiate" 5 "Definition" rhs
let simpleDef = MkPMDefInfo (SolvedHole num) (isSimple rhs) False
let simpleDef = MkPMDefInfo (SolvedHole num)
(not (isUserName mname) && isSimple rhs)
False
let newdef = record { definition =
PMDef simpleDef [] (STerm 0 rhs) (STerm 0 rhs) []
} mdef