edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-24 04:43:25 +03:00
Code Issues Projects Releases Wiki Activity

Simplify the definition of processFnOpt

Browse Source 
There's no need to split into cases for the totality annotations, as
they now use the same representation in the AST as in `TT`.
This commit is contained in:
Ohad Kammar 2020-02-23 16:44:23 +00:00
parent b7ba1a9301
commit 9da96dd586
1 changed files with 2 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/TTImp/ProcessType.idr
View File

@ -46,12 +46,8 @@ processFnOpt fc ndef (ForeignFn _)
= setFlag fc ndef Inline -- if externally defined, inline when compiling
processFnOpt fc ndef Invertible
= setFlag fc ndef Invertible
processFnOpt fc ndef (Totality Total)
= setFlag fc ndef (SetTotal Total)
processFnOpt fc ndef (Totality Covering)
= setFlag fc ndef (SetTotal CoveringOnly)
processFnOpt fc ndef (Totality PartialOK)
= setFlag fc ndef (SetTotal PartialOK)
processFnOpt fc ndef (Totality tot)
= setFlag fc ndef (SetTotal tot)
processFnOpt fc ndef Macro
= setFlag fc ndef Macro