mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-11 13:36:08 +03:00
Merge pull request #3150 from dunhamsteve/defaulthint-error
[ error ] Fix error message for %defaulthint on a local function
This commit is contained in:
commit
737a2d96dd
@ -49,7 +49,9 @@ processFnOpt fc _ ndef (Hint d)
|
||||
addLocalHint ndef
|
||||
processFnOpt fc True ndef (GlobalHint a)
|
||||
= addGlobalHint ndef a
|
||||
processFnOpt fc _ ndef (GlobalHint a)
|
||||
processFnOpt fc _ ndef (GlobalHint True)
|
||||
= throw (GenericMsg fc "%defaulthint is not valid in local definitions")
|
||||
processFnOpt fc _ ndef (GlobalHint False)
|
||||
= throw (GenericMsg fc "%globalhint is not valid in local definitions")
|
||||
processFnOpt fc _ ndef ExternFn
|
||||
= setFlag fc ndef Inline -- if externally defined, inline when compiling
|
||||
|
Loading…
Reference in New Issue
Block a user