mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-28 11:05:17 +03:00
Bugfix 654: forgot to update GenerateDef
When synthesizing clauses, allow synthesised clauses to be partial. It's an arbitrary choice, the other choice can be the default option. But if the place in which we're synthesising has a non-default choice, then we're synthesising under the wrong option too.
This commit is contained in:
parent
2f5ae26f36
commit
b2a9ba651c
@ -56,7 +56,7 @@ expandClause : {auto c : Ref Ctxt Defs} ->
|
||||
Core (Search (List ImpClause))
|
||||
expandClause loc opts n c
|
||||
= do c <- uniqueRHS c
|
||||
Right clause <- checkClause linear Private False n [] (MkNested []) [] c
|
||||
Right clause <- checkClause linear Private PartialOK False n [] (MkNested []) [] c
|
||||
| Left err => noResult -- TODO: impossible clause, do something
|
||||
-- appropriate
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user