From 9da96dd586a61ca417abcbea304102869f5605ca Mon Sep 17 00:00:00 2001 From: Ohad Kammar Date: Sun, 23 Feb 2020 16:44:23 +0000 Subject: [PATCH] Simplify the definition of `processFnOpt` 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`. --- src/TTImp/ProcessType.idr | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/TTImp/ProcessType.idr b/src/TTImp/ProcessType.idr index 86f3d61..d57ec7b 100644 --- a/src/TTImp/ProcessType.idr +++ b/src/TTImp/ProcessType.idr @@ -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