mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-11 13:36:08 +03:00
[ error ] Fix error message for %defaulthint on a local function
This commit is contained in:
parent
b65064a913
commit
1f54d68e86
@ -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