7f8a4cb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fixed addition of partiality by default in order to avoid not interfering with --warn-partial

commit7f8a4cb0f2ebf79fb16dd40c372223b80320ec93 authorAhmad Salim Al-Sibahi <asal@itu.dk> dateSat 7 May 2016, 20:32 (10 years ago) parentc5f2052

1 file changed+1−1

unifiedsplit

src/Idris/Parser.hs+1−1

@@ -650,7 +650,7 @@ fnOpts = do

650650 case default_total ist of

651651 DefaultCheckingTotal -> return (TotalFn:opts)

652652 DefaultCheckingCovering -> return (CoveringFn:opts)

653− DefaultCheckingPartial -> return (PartialFn:opts)

653+ DefaultCheckingPartial -> return opts -- Don't add partial so that --warn-partial still reports warnings if necessary

654654 addDefaultTotality [tot] opts = return opts

655655 -- Should really be a semantics error instead of a parser error

656656 addDefaultTotality (tot1:tot2:tots) opts =