diff --git a/app/Main.hs b/app/Main.hs
index c61b51a5b..68f0eec7a 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -2,8 +2,6 @@
 
 module Main (main) where
 
---------------------------------------------------------------------------------
-
 import Commands.Extra
 import Commands.MicroJuvix
 import Commands.MiniHaskell
@@ -432,24 +430,30 @@ runCLI cli = do
       minihaskell <- head . (^. MiniHaskell.resultModules) <$> runIO (upToMiniHaskell (getEntryPoint root o))
       renderStdOutMini (MiniHaskell.ppOutDefault minihaskell)
     Termination (Calls opts@CallsOptions {..}) -> do
-      a <- head . (^. Abstract.resultModules) <$> runIO (upToAbstract (getEntryPoint root opts))
-      let callMap0 = T.buildCallMap a
+      results <- runIO (upToAbstract (getEntryPoint root opts))
+      let topModule = head (results ^. Abstract.resultModules)
+          infotable = results ^. Abstract.resultTable
+          callMap0 = T.buildCallMap infotable topModule
           callMap = case _callsFunctionNameFilter of
             Nothing -> callMap0
             Just f -> T.filterCallMap f callMap0
           opts' = T.callsPrettyOptions opts
       renderStdOutAbs (Abstract.ppOut opts' callMap)
       putStrLn ""
-    Termination (CallGraph o@CallGraphOptions {..}) -> do
-      a <- head . (^. Abstract.resultModules) <$> runIO (upToAbstract (getEntryPoint root o))
-      let callMap = T.buildCallMap a
+    Termination (CallGraph opts@CallGraphOptions {..}) -> do
+      results <- runIO (upToAbstract (getEntryPoint root opts))
+      let topModule = head (results ^. Abstract.resultModules)
+          infotable = results ^. Abstract.resultTable
+          callMap = T.buildCallMap infotable topModule
           opts' =
             Abstract.defaultOptions
               { Abstract._optShowNameId = globalOptions ^. globalShowNameIds
               }
           completeGraph = T.completeCallGraph callMap
           filteredGraph = maybe completeGraph (`T.unsafeFilterGraph` completeGraph) _graphFunctionNameFilter
-          recBehav = map T.recursiveBehaviour (T.reflexiveEdges filteredGraph)
+          rEdges = T.reflexiveEdges filteredGraph
+
+          recBehav = map T.recursiveBehaviour rEdges
       renderStdOutAbs (Abstract.ppOut opts' filteredGraph)
       putStrLn ""
       forM_ recBehav $ \r -> do
@@ -457,11 +461,11 @@ runCLI cli = do
               Scoper.defaultOptions
                 { Scoper._optShowNameId = globalOptions ^. globalShowNameIds
                 }
-            n = toAnsiText' (Scoper.ppOut sopts (A._recBehaviourFunction r))
+            n = toAnsiText' (Scoper.ppOut sopts (A._recursiveBehaviourFun r))
         renderStdOutAbs (Abstract.ppOut opts' r)
         putStrLn ""
         case T.findOrder r of
-          Nothing -> putStrLn (n <> " Fails the termination checking")
+          Nothing -> putStrLn (n <> " Fails the termination checking") >> exitFailure
           Just (T.LexOrder k) -> putStrLn (n <> " Terminates with order " <> show (toList k))
         putStrLn ""
 
diff --git a/lab/Syntax/Core.hs b/lab/Syntax/Core.hs
index 776ebf985..ad66d3982 100644
--- a/lab/Syntax/Core.hs
+++ b/lab/Syntax/Core.hs
@@ -4,9 +4,6 @@
 
 module MiniJuvix.Syntax.Core where
 
---------------------------------------------------------------------------------
-
--- import Algebra.Graph.Label (Semiring (..))
 import MiniJuvix.Prelude hiding (Local)
 import Numeric.Natural (Natural)
 
diff --git a/src/MiniJuvix/Internal/Strings.hs b/src/MiniJuvix/Internal/Strings.hs
index 285f1478b..48592dfd6 100644
--- a/src/MiniJuvix/Internal/Strings.hs
+++ b/src/MiniJuvix/Internal/Strings.hs
@@ -77,6 +77,9 @@ any = "Any"
 type_ :: IsString s => s
 type_ = "Type"
 
+questionMark :: IsString s => s
+questionMark = "?"
+
 keyword :: IsString s => s
 keyword = "keyword"
 
@@ -154,3 +157,9 @@ ghc = "ghc"
 
 agda :: IsString s => s
 agda = "agda"
+
+terminating :: IsString s => s
+terminating = "terminating"
+
+waveArrow :: IsString s => s
+waveArrow = "↝"
diff --git a/src/MiniJuvix/Prelude/Base.hs b/src/MiniJuvix/Prelude/Base.hs
index af31db95f..3e81da617 100644
--- a/src/MiniJuvix/Prelude/Base.hs
+++ b/src/MiniJuvix/Prelude/Base.hs
@@ -63,8 +63,6 @@ module MiniJuvix.Prelude.Base
   )
 where
 
---------------------------------------------------------------------------------
-
 import Control.Applicative
 import Control.Monad.Extra
 import Control.Monad.Fix
@@ -87,7 +85,18 @@ import Data.Int
 import Data.List.Extra hiding (groupSortOn, head, last, mconcatMap)
 import Data.List.Extra qualified as List
 import Data.List.NonEmpty qualified as NonEmpty
-import Data.List.NonEmpty.Extra (NonEmpty (..), head, last, maximum1, maximumOn1, minimum1, minimumOn1, nonEmpty, some1, (|:))
+import Data.List.NonEmpty.Extra
+  ( NonEmpty (..),
+    head,
+    last,
+    maximum1,
+    maximumOn1,
+    minimum1,
+    minimumOn1,
+    nonEmpty,
+    some1,
+    (|:),
+  )
 import Data.Maybe
 import Data.Monoid
 import Data.Ord
@@ -125,27 +134,24 @@ import Safe.Foldable
 import System.Directory
 import System.Exit
 import System.FilePath
-import System.IO hiding (appendFile, getContents, getLine, hGetContents, hGetLine, hPutStr, hPutStrLn, interact, putStr, putStrLn, readFile, readFile', writeFile)
+import System.IO hiding
+  ( appendFile,
+    getContents,
+    getLine,
+    hGetContents,
+    hGetLine,
+    hPutStr,
+    hPutStrLn,
+    interact,
+    putStr,
+    putStrLn,
+    readFile,
+    readFile',
+    writeFile,
+  )
 import Text.Show (Show)
 import Text.Show qualified as Show
 
---------------------------------------------------------------------------------
--- Logical connectives
---------------------------------------------------------------------------------
-
-(∨) :: Bool -> Bool -> Bool
-(∨) = (||)
-
-infixr 2 ∨
-
-(∧) :: Bool -> Bool -> Bool
-(∧) = (&&)
-
-infixr 3 ∧
-
-(.||.) :: (a -> Bool) -> (a -> Bool) -> a -> Bool
-(f .||. g) x = f x || g x
-
 --------------------------------------------------------------------------------
 -- High-level syntax sugar.
 --------------------------------------------------------------------------------
@@ -249,8 +255,6 @@ undefined = Err.error "undefined"
 impossible :: HasCallStack => a
 impossible = Err.error "impossible"
 
---------------------------------------------------------------------------------
--- Errors
 --------------------------------------------------------------------------------
 
 infixl 7 <+?>
@@ -263,6 +267,8 @@ infixl 7 <?>
 (<?>) :: Semigroup m => m -> Maybe m -> m
 (<?>) a = maybe a (a <>)
 
+--------------------------------------------------------------------------------
+
 data Indexed a = Indexed
   { _indexedIx :: Int,
     _indexedThing :: a
diff --git a/src/MiniJuvix/Prelude/Pretty.hs b/src/MiniJuvix/Prelude/Pretty.hs
index 4186ba036..ac7f432a4 100644
--- a/src/MiniJuvix/Prelude/Pretty.hs
+++ b/src/MiniJuvix/Prelude/Pretty.hs
@@ -35,6 +35,9 @@ prettyText = Text.renderStrict . layoutPretty defaultLayoutOptions . pretty
 vsep :: Foldable f => f (Doc a) -> Doc a
 vsep = PP.vsep . toList
 
+vsep2 :: [Doc a] -> Doc a
+vsep2 = concatWith (\a b -> a <> line <> line <> b)
+
 hsep :: Foldable f => f (Doc a) -> Doc a
 hsep = PP.hsep . toList
 
diff --git a/src/MiniJuvix/Syntax/Abstract/InfoTable.hs b/src/MiniJuvix/Syntax/Abstract/InfoTable.hs
index 4289fd579..e0c0cfd76 100644
--- a/src/MiniJuvix/Syntax/Abstract/InfoTable.hs
+++ b/src/MiniJuvix/Syntax/Abstract/InfoTable.hs
@@ -7,6 +7,7 @@ import MiniJuvix.Syntax.Concrete.Scoped.Name qualified as S
 newtype FunctionInfo = FunctionInfo
   { _functionInfoDef :: FunctionDef
   }
+  deriving stock (Show)
 
 data ConstructorInfo = ConstructorInfo
   { _constructorInfoInductive :: InductiveInfo,
diff --git a/src/MiniJuvix/Syntax/Abstract/Language.hs b/src/MiniJuvix/Syntax/Abstract/Language.hs
index 6a9402e9e..6db3e2de3 100644
--- a/src/MiniJuvix/Syntax/Abstract/Language.hs
+++ b/src/MiniJuvix/Syntax/Abstract/Language.hs
@@ -57,7 +57,8 @@ data Statement
 data FunctionDef = FunctionDef
   { _funDefName :: FunctionName,
     _funDefTypeSig :: Expression,
-    _funDefClauses :: NonEmpty FunctionClause
+    _funDefClauses :: NonEmpty FunctionClause,
+    _funDefTerminating :: Bool
   }
   deriving stock (Eq, Show)
 
diff --git a/src/MiniJuvix/Syntax/Abstract/Language/Extra.hs b/src/MiniJuvix/Syntax/Abstract/Language/Extra.hs
index 371a5a447..cee983da2 100644
--- a/src/MiniJuvix/Syntax/Abstract/Language/Extra.hs
+++ b/src/MiniJuvix/Syntax/Abstract/Language/Extra.hs
@@ -7,22 +7,22 @@ where
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Abstract.Language
 
+patternVariables :: Pattern -> [VarName]
+patternVariables pat = case pat of
+  PatternVariable v -> [v]
+  PatternWildcard {} -> []
+  PatternEmpty {} -> []
+  PatternConstructorApp app -> appVariables app
+
+appVariables :: ConstructorApp -> [VarName]
+appVariables (ConstructorApp _ ps) = concatMap patternVariables ps
+
 smallerPatternVariables :: Pattern -> [VarName]
-smallerPatternVariables p = case p of
+smallerPatternVariables = \case
   PatternVariable {} -> []
   PatternWildcard {} -> []
   PatternEmpty {} -> []
   PatternConstructorApp app -> appVariables app
-  where
-    appVariables :: ConstructorApp -> [VarName]
-    appVariables (ConstructorApp _ ps) = concatMap patternVariables ps
-
-    patternVariables :: Pattern -> [VarName]
-    patternVariables pat = case pat of
-      PatternVariable v -> [v]
-      PatternWildcard {} -> []
-      PatternEmpty {} -> []
-      PatternConstructorApp app -> appVariables app
 
 viewApp :: Expression -> (Expression, [Expression])
 viewApp e = case e of
diff --git a/src/MiniJuvix/Syntax/Abstract/Pretty/Base.hs b/src/MiniJuvix/Syntax/Abstract/Pretty/Base.hs
index 12c0c16ba..fcb1d3376 100644
--- a/src/MiniJuvix/Syntax/Abstract/Pretty/Base.hs
+++ b/src/MiniJuvix/Syntax/Abstract/Pretty/Base.hs
@@ -44,31 +44,17 @@ ppDefault = runPrettyCode defaultOptions
 runPrettyCode :: PrettyCode c => Options -> c -> Doc Ann
 runPrettyCode opts = run . runReader opts . ppCode
 
-instance PrettyCode Iden where
-  ppCode = ppSCode . idenName
-
-instance PrettyCode Application where
-  ppCode (Application l r) = do
-    l' <- ppLeftExpression appFixity l
-    r' <- ppRightExpression appFixity r
-    return $ l' <+> r'
-
 keyword :: Text -> Doc Ann
 keyword = annotate AnnKeyword . pretty
 
 kwType :: Doc Ann
 kwType = keyword Str.type_
 
-instance PrettyCode Universe where
-  ppCode (Universe n) = return $ kwType <+?> (pretty <$> n)
+kwQuestion :: Doc Ann
+kwQuestion = keyword Str.questionMark
 
-instance PrettyCode Expression where
-  ppCode e = case e of
-    ExpressionIden i -> ppCode i
-    ExpressionUniverse u -> ppCode u
-    ExpressionApplication a -> ppCode a
-    ExpressionFunction f -> ppCode f
-    ExpressionLiteral l -> ppSCode l
+kwWaveArrow :: Doc Ann
+kwWaveArrow = keyword Str.waveArrow
 
 kwColon :: Doc Ann
 kwColon = keyword Str.colon
@@ -85,40 +71,6 @@ kwColonOne = keyword Str.colonOne
 kwColonOmega :: Doc Ann
 kwColonOmega = keyword Str.colonOmegaUnicode
 
-instance PrettyCode Usage where
-  ppCode u = return $ case u of
-    UsageNone -> kwColonZero
-    UsageOnce -> kwColonOne
-    UsageOmega -> kwColon
-
-instance PrettyCode FunctionParameter where
-  ppCode FunctionParameter {..} = do
-    case _paramName of
-      Nothing -> ppLeftExpression funFixity _paramType
-      Just n -> do
-        paramName' <- ppSCode n
-        paramType' <- ppCode _paramType
-        paramUsage' <- ppCode _paramUsage
-        return $ parens (paramName' <+> paramUsage' <+> paramType')
-
-instance PrettyCode Function where
-  ppCode Function {..} = do
-    funParameter' <- ppCode _funParameter
-    funReturn' <- ppRightExpression funFixity _funReturn
-    return $ funParameter' <+> kwTo <+> funReturn'
-
-instance PrettyCode FunctionRef where
-  ppCode FunctionRef {..} = ppSCode _functionRefName
-
-instance PrettyCode ConstructorRef where
-  ppCode ConstructorRef {..} = ppSCode _constructorRefName
-
-instance PrettyCode InductiveRef where
-  ppCode InductiveRef {..} = ppSCode _inductiveRefName
-
-instance PrettyCode AxiomRef where
-  ppCode AxiomRef {..} = ppSCode _axiomRefName
-
 parensCond :: Bool -> Doc Ann -> Doc Ann
 parensCond t d = if t then parens d else d
 
@@ -153,7 +105,64 @@ ppLRExpression associates fixlr e =
   parensCond (atomParens associates (atomicity e) fixlr)
     <$> ppCode e
 
-ppCodeAtom :: (HasAtomicity c, PrettyCode c, Members '[Reader Options] r) => c -> Sem r (Doc Ann)
+ppCodeAtom ::
+  (HasAtomicity c, PrettyCode c, Members '[Reader Options] r) =>
+  c ->
+  Sem r (Doc Ann)
 ppCodeAtom c = do
   p' <- ppCode c
   return $ if isAtomic c then p' else parens p'
+
+instance PrettyCode Iden where
+  ppCode = ppSCode . idenName
+
+instance PrettyCode Application where
+  ppCode (Application l r) = do
+    l' <- ppLeftExpression appFixity l
+    r' <- ppRightExpression appFixity r
+    return $ l' <+> r'
+
+instance PrettyCode Universe where
+  ppCode (Universe n) = return $ kwType <+?> (pretty <$> n)
+
+instance PrettyCode Expression where
+  ppCode e = case e of
+    ExpressionIden i -> ppCode i
+    ExpressionUniverse u -> ppCode u
+    ExpressionApplication a -> ppCode a
+    ExpressionFunction f -> ppCode f
+    ExpressionLiteral l -> ppSCode l
+
+instance PrettyCode Usage where
+  ppCode u = return $ case u of
+    UsageNone -> kwColonZero
+    UsageOnce -> kwColonOne
+    UsageOmega -> kwColon
+
+instance PrettyCode FunctionParameter where
+  ppCode FunctionParameter {..} = do
+    case _paramName of
+      Nothing -> ppLeftExpression funFixity _paramType
+      Just n -> do
+        paramName' <- ppSCode n
+        paramType' <- ppCode _paramType
+        paramUsage' <- ppCode _paramUsage
+        return $ parens (paramName' <+> paramUsage' <+> paramType')
+
+instance PrettyCode Function where
+  ppCode Function {..} = do
+    funParameter' <- ppCode _funParameter
+    funReturn' <- ppRightExpression funFixity _funReturn
+    return $ funParameter' <+> kwTo <+> funReturn'
+
+instance PrettyCode FunctionRef where
+  ppCode FunctionRef {..} = ppSCode _functionRefName
+
+instance PrettyCode ConstructorRef where
+  ppCode ConstructorRef {..} = ppSCode _constructorRefName
+
+instance PrettyCode InductiveRef where
+  ppCode InductiveRef {..} = ppSCode _inductiveRefName
+
+instance PrettyCode AxiomRef where
+  ppCode AxiomRef {..} = ppSCode _axiomRefName
diff --git a/src/MiniJuvix/Syntax/Concrete/Language.hs b/src/MiniJuvix/Syntax/Concrete/Language.hs
index 05d0d79fd..d0c3642f5 100644
--- a/src/MiniJuvix/Syntax/Concrete/Language.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Language.hs
@@ -17,8 +17,6 @@ module MiniJuvix.Syntax.Concrete.Language
   )
 where
 
---------------------------------------------------------------------------------
-
 import Data.Kind qualified as GHC
 import MiniJuvix.Prelude hiding (show)
 import MiniJuvix.Syntax.Backends
@@ -176,7 +174,8 @@ instance HasLoc OperatorSyntaxDef where
 
 data TypeSignature (s :: Stage) = TypeSignature
   { _sigName :: FunctionName s,
-    _sigType :: ExpressionType s
+    _sigType :: ExpressionType s,
+    _sigTerminating :: Bool
   }
 
 deriving stock instance (Show (ExpressionType s), Show (SymbolType s)) => Show (TypeSignature s)
diff --git a/src/MiniJuvix/Syntax/Concrete/Lexer.hs b/src/MiniJuvix/Syntax/Concrete/Lexer.hs
index b2ef330c4..2c960479d 100644
--- a/src/MiniJuvix/Syntax/Concrete/Lexer.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Lexer.hs
@@ -1,7 +1,5 @@
 module MiniJuvix.Syntax.Concrete.Lexer where
 
---------------------------------------------------------------------------------
-
 import Data.Text qualified as Text
 import GHC.Unicode
 import MiniJuvix.Internal.Strings qualified as Str
@@ -259,6 +257,9 @@ kwSemicolon = keyword Str.semicolon
 kwType :: Member InfoTableBuilder r => ParsecS r ()
 kwType = keyword Str.type_
 
+kwTerminating :: Member InfoTableBuilder r => ParsecS r ()
+kwTerminating = keyword Str.terminating
+
 kwUsing :: Member InfoTableBuilder r => ParsecS r ()
 kwUsing = keyword Str.using
 
diff --git a/src/MiniJuvix/Syntax/Concrete/Parser.hs b/src/MiniJuvix/Syntax/Concrete/Parser.hs
index 4bd40f398..de9333d33 100644
--- a/src/MiniJuvix/Syntax/Concrete/Parser.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Parser.hs
@@ -247,8 +247,7 @@ match = do
 --------------------------------------------------------------------------------
 
 letClause :: Member InfoTableBuilder r => ParsecS r (LetClause 'Parsed)
-letClause = do
-  either LetTypeSig LetFunClause <$> auxTypeSigFunClause
+letClause = either LetTypeSig LetFunClause <$> auxTypeSigFunClause
 
 letBlock :: Member InfoTableBuilder r => ParsecS r (LetBlock 'Parsed)
 letBlock = do
@@ -271,8 +270,12 @@ universe = do
 -- Type signature declaration
 -------------------------------------------------------------------------------
 
-typeSignature :: Member InfoTableBuilder r => Symbol -> ParsecS r (TypeSignature 'Parsed)
-typeSignature _sigName = do
+typeSignature ::
+  Member InfoTableBuilder r =>
+  Bool ->
+  Symbol ->
+  ParsecS r (TypeSignature 'Parsed)
+typeSignature _sigTerminating _sigName = do
   kwColon
   _sigType <- expressionAtoms
   return TypeSignature {..}
@@ -286,9 +289,10 @@ auxTypeSigFunClause ::
   Member InfoTableBuilder r =>
   ParsecS r (Either (TypeSignature 'Parsed) (FunctionClause 'Parsed))
 auxTypeSigFunClause = do
-  s <- symbol
-  (Left <$> typeSignature s)
-    <|> (Right <$> functionClause s)
+  terminating <- isJust <$> optional kwTerminating
+  sym <- symbol
+  (Left <$> typeSignature terminating sym)
+    <|> (Right <$> functionClause sym)
 
 -------------------------------------------------------------------------------
 -- Axioms
diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs
index 4ec2e7ee8..8f910bc84 100644
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs
@@ -404,7 +404,7 @@ checkTypeSignature ::
 checkTypeSignature TypeSignature {..} = do
   sigType' <- checkParseExpressionAtoms _sigType
   sigName' <- bindFunctionSymbol _sigName
-  registerFunction' TypeSignature {_sigName = sigName', _sigType = sigType'}
+  registerFunction' TypeSignature {_sigName = sigName', _sigType = sigType', ..}
 
 checkConstructorDef ::
   Members '[Error ScopeError, Reader LocalVars, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
diff --git a/src/MiniJuvix/Syntax/MiniHaskell/Pretty/Base.hs b/src/MiniJuvix/Syntax/MiniHaskell/Pretty/Base.hs
index e6d6323eb..0809b95f0 100644
--- a/src/MiniJuvix/Syntax/MiniHaskell/Pretty/Base.hs
+++ b/src/MiniJuvix/Syntax/MiniHaskell/Pretty/Base.hs
@@ -7,6 +7,7 @@ where
 
 import MiniJuvix.Internal.Strings qualified as Str
 import MiniJuvix.Prelude
+import MiniJuvix.Prelude.Pretty qualified as PP
 import MiniJuvix.Syntax.Concrete.Language (Literal (..), LiteralLoc (..))
 import MiniJuvix.Syntax.Fixity
 import MiniJuvix.Syntax.MiniHaskell.Language
@@ -139,9 +140,7 @@ instance PrettyCode Statement where
 instance PrettyCode ModuleBody where
   ppCode m = do
     statements' <- mapM ppCode (m ^. moduleStatements)
-    return $ vsep2 statements'
-    where
-      vsep2 = concatWith (\a b -> a <> line <> line <> b)
+    return $ PP.vsep2 statements'
 
 instance PrettyCode Literal where
   ppCode = \case
diff --git a/src/MiniJuvix/Syntax/MonoJuvix/Pretty/Base.hs b/src/MiniJuvix/Syntax/MonoJuvix/Pretty/Base.hs
index fd48deeb7..d9fa8beb6 100644
--- a/src/MiniJuvix/Syntax/MonoJuvix/Pretty/Base.hs
+++ b/src/MiniJuvix/Syntax/MonoJuvix/Pretty/Base.hs
@@ -235,8 +235,6 @@ instance PrettyCode ModuleBody where
   ppCode m = do
     everything <- mapM ppCode (m ^. moduleStatements)
     return $ vsep2 everything
-    where
-      vsep2 = concatWith (\a b -> a <> line <> line <> b)
 
 instance PrettyCode Module where
   ppCode m = do
diff --git a/src/MiniJuvix/Termination/CallGraph.hs b/src/MiniJuvix/Termination/CallGraph.hs
index bea85a5cb..c59705c57 100644
--- a/src/MiniJuvix/Termination/CallGraph.hs
+++ b/src/MiniJuvix/Termination/CallGraph.hs
@@ -7,13 +7,14 @@ where
 import Data.HashMap.Strict qualified as HashMap
 import Data.HashSet qualified as HashSet
 import MiniJuvix.Prelude
+import MiniJuvix.Prelude.Pretty
 import MiniJuvix.Syntax.Abstract.Language.Extra
 import MiniJuvix.Syntax.Abstract.Pretty.Base
 import MiniJuvix.Syntax.Concrete.Scoped.Name qualified as S
 import MiniJuvix.Termination.Types
 import Prettyprinter as PP
 
-type Edges = HashMap (FunctionName, FunctionName) Edge
+type Graph = HashMap (FunctionName, FunctionName) Edge
 
 data Edge = Edge
   { _edgeFrom :: FunctionName,
@@ -21,37 +22,28 @@ data Edge = Edge
     _edgeMatrices :: HashSet CallMatrix
   }
 
-newtype CompleteCallGraph = CompleteCallGraph Edges
+newtype CompleteCallGraph = CompleteCallGraph Graph
 
 data ReflexiveEdge = ReflexiveEdge
-  { _redgeFun :: FunctionName,
-    _redgeMatrices :: HashSet CallMatrix
+  { _reflexiveEdgeFun :: FunctionName,
+    _reflexiveEdgeMatrices :: HashSet CallMatrix
   }
 
 data RecursiveBehaviour = RecursiveBehaviour
-  { _recBehaviourFunction :: FunctionName,
-    _recBehaviourMatrix :: [[Rel]]
+  { _recursiveBehaviourFun :: FunctionName,
+    _recursiveBehaviourMatrix :: [[Rel]]
   }
 
-makeLenses ''RecursiveBehaviour
 makeLenses ''Edge
+makeLenses ''RecursiveBehaviour
 makeLenses ''ReflexiveEdge
 
-multiply :: CallMatrix -> CallMatrix -> CallMatrix
-multiply a b = map sumProdRow a
-  where
-    rowB :: Int -> CallRow
-    rowB i = CallRow $ case b !? i of
-      Just (CallRow (Just c)) -> Just c
-      _ -> Nothing
-    sumProdRow :: CallRow -> CallRow
-    sumProdRow (CallRow mr) = CallRow $ do
-      (ki, ra) <- mr
-      (j, rb) <- _callRow (rowB ki)
-      return (j, mul' ra rb)
+-------------------------------------------------------------------------------
+-- Misc
+-------------------------------------------------------------------------------
 
-multiplyMany :: HashSet CallMatrix -> HashSet CallMatrix -> HashSet CallMatrix
-multiplyMany r s = HashSet.fromList [multiply a b | a <- toList r, b <- toList s]
+fromEdgeList :: [Edge] -> Graph
+fromEdgeList l = HashMap.fromList [((e ^. edgeFrom, e ^. edgeTo), e) | e <- l]
 
 composeEdge :: Edge -> Edge -> Maybe Edge
 composeEdge a b = do
@@ -63,6 +55,44 @@ composeEdge a b = do
         _edgeMatrices = multiplyMany (a ^. edgeMatrices) (b ^. edgeMatrices)
       }
 
+edgesCompose :: Graph -> Graph -> Graph
+edgesCompose g h =
+  fromEdgeList
+    (catMaybes [composeEdge u v | u <- toList g, v <- toList h])
+
+edgeUnion :: Edge -> Edge -> Edge
+edgeUnion a b
+  | a ^. edgeFrom == b ^. edgeFrom,
+    a ^. edgeTo == b ^. edgeTo =
+      Edge
+        (a ^. edgeFrom)
+        (a ^. edgeTo)
+        (HashSet.union (a ^. edgeMatrices) (b ^. edgeMatrices))
+  | otherwise = impossible
+
+edgesUnion :: Graph -> Graph -> Graph
+edgesUnion = HashMap.unionWith edgeUnion
+
+edgesCount :: Graph -> Int
+edgesCount es = sum [HashSet.size (e ^. edgeMatrices) | e <- toList es]
+
+multiply :: CallMatrix -> CallMatrix -> CallMatrix
+multiply a b = map sumProdRow a
+  where
+    rowB :: Int -> CallRow
+    rowB i = CallRow $ case b !? i of
+      Just (CallRow (Just c)) -> Just c
+      _ -> Nothing
+
+    sumProdRow :: CallRow -> CallRow
+    sumProdRow (CallRow mr) = CallRow $ do
+      (ki, ra) <- mr
+      (j, rb) <- _callRow (rowB ki)
+      return (j, mul' ra rb)
+
+multiplyMany :: HashSet CallMatrix -> HashSet CallMatrix -> HashSet CallMatrix
+multiplyMany r s = HashSet.fromList [multiply a b | a <- toList r, b <- toList s]
+
 fromFunCall :: FunctionRef -> FunCall -> Call
 fromFunCall caller fc =
   Call
@@ -78,61 +108,37 @@ unsafeFilterGraph funNames (CompleteCallGraph g) =
   CompleteCallGraph (HashMap.filterWithKey (\(f, _) _ -> S.symbolText f `elem` funNames) g)
 
 completeCallGraph :: CallMap -> CompleteCallGraph
-completeCallGraph cm = CompleteCallGraph (go startingEdges)
+completeCallGraph CallMap {..} = CompleteCallGraph (go startingEdges)
   where
-    startingEdges :: Edges
+    startingEdges :: Graph
     startingEdges = foldr insertCall mempty allCalls
       where
-        insertCall :: Call -> Edges -> Edges
+        insertCall :: Call -> Graph -> Graph
         insertCall Call {..} = HashMap.alter (Just . aux) (_callFrom, _callTo)
           where
             aux :: Maybe Edge -> Edge
             aux me = case me of
               Nothing -> Edge _callFrom _callTo (HashSet.singleton _callMatrix)
               Just e -> over edgeMatrices (HashSet.insert _callMatrix) e
+
     allCalls :: [Call]
     allCalls =
       [ fromFunCall caller funCall
-        | (caller, callerMap) <- HashMap.toList (cm ^. callMap),
+        | (caller, callerMap) <- HashMap.toList _callMap,
           (_, funCalls) <- HashMap.toList callerMap,
           funCall <- funCalls
       ]
 
-    go :: Edges -> Edges
-    go m
-      | edgesCount m == edgesCount m' = m
-      | otherwise = go m'
+    go :: Graph -> Graph
+    go g
+      | edgesCount g == edgesCount g' = g
+      | otherwise = go g'
       where
-        m' = step m
+        g' = step g
 
-    step :: Edges -> Edges
+    step :: Graph -> Graph
     step s = edgesUnion (edgesCompose s startingEdges) s
 
-    fromEdgeList :: [Edge] -> Edges
-    fromEdgeList l = HashMap.fromList [((e ^. edgeFrom, e ^. edgeTo), e) | e <- l]
-
-    edgesCompose :: Edges -> Edges -> Edges
-    edgesCompose a b =
-      fromEdgeList $
-        catMaybes
-          [composeEdge ea eb | ea <- toList a, eb <- toList b]
-
-    edgeUnion :: Edge -> Edge -> Edge
-    edgeUnion a b
-      | a ^. edgeFrom == b ^. edgeFrom,
-        a ^. edgeTo == b ^. edgeTo =
-          Edge
-            (a ^. edgeFrom)
-            (a ^. edgeTo)
-            (HashSet.union (a ^. edgeMatrices) (b ^. edgeMatrices))
-      | otherwise = impossible
-
-    edgesUnion :: Edges -> Edges -> Edges
-    edgesUnion = HashMap.unionWith edgeUnion
-
-    edgesCount :: Edges -> Int
-    edgesCount es = sum [HashSet.size (e ^. edgeMatrices) | e <- toList es]
-
 reflexiveEdges :: CompleteCallGraph -> [ReflexiveEdge]
 reflexiveEdges (CompleteCallGraph es) = mapMaybe reflexive (toList es)
   where
@@ -155,14 +161,15 @@ callMatrixDiag m = [col i r | (i, r) <- zip [0 :: Int ..] m]
 recursiveBehaviour :: ReflexiveEdge -> RecursiveBehaviour
 recursiveBehaviour re =
   RecursiveBehaviour
-    (re ^. redgeFun)
-    (map callMatrixDiag (toList $ re ^. redgeMatrices))
+    (re ^. reflexiveEdgeFun)
+    (map callMatrixDiag (toList $ re ^. reflexiveEdgeMatrices))
 
 findOrder :: RecursiveBehaviour -> Maybe LexOrder
 findOrder rb = LexOrder <$> listToMaybe (mapMaybe (isLexOrder >=> nonEmpty) allPerms)
   where
     b0 :: [[Rel]]
-    b0 = rb ^. recBehaviourMatrix
+    b0 = rb ^. recursiveBehaviourMatrix
+
     indexed = map (zip [0 :: Int ..] . take minLength) b0
       where
         minLength = minimum (map length b0)
@@ -204,29 +211,32 @@ instance PrettyCode Edge where
   ppCode Edge {..} = do
     fromFun <- ppSCode _edgeFrom
     toFun <- ppSCode _edgeTo
-    matrices <- indent 2 . ppMatrices . zip [0 :: Int ..] <$> mapM ppCode (toList _edgeMatrices)
+    matrices <-
+      indent 2 . ppMatrices . zip [0 :: Int ..]
+        <$> mapM ppCode (toList _edgeMatrices)
     return $
-      pretty ("Edge" :: Text) <+> fromFun <+> waveFun <+> toFun <> line
+      pretty ("Edge" :: Text) <+> fromFun <+> kwWaveArrow <+> toFun <> line
         <> matrices
     where
       ppMatrices = vsep2 . map ppMatrix
       ppMatrix (i, t) =
-        pretty ("Matrix" :: Text) <+> pretty i <> colon <> line
-          <> t
+        pretty ("Matrix" :: Text) <+> pretty i <> colon <> line <> t
 
 instance PrettyCode CompleteCallGraph where
   ppCode :: forall r. Members '[Reader Options] r => CompleteCallGraph -> Sem r (Doc Ann)
-  ppCode (CompleteCallGraph edges) = do
-    es <- vsep2 <$> mapM ppCode (toList edges)
-    return $ pretty ("Complete Call Graph:" :: Text) <> line <> es
+  ppCode (CompleteCallGraph edges)
+    | null edges = return $ pretty ("Empty graph" :: Text)
+    | otherwise = do
+        es <- vsep2 <$> mapM ppCode (toList edges)
+        return $ pretty ("Complete call graph:" :: Text) <> line <> es <> pretty (length edges)
 
 instance PrettyCode RecursiveBehaviour where
-  ppCode :: forall r. Members '[Reader Options] r => RecursiveBehaviour -> Sem r (Doc Ann)
+  ppCode :: Members '[Reader Options] r => RecursiveBehaviour -> Sem r (Doc Ann)
   ppCode (RecursiveBehaviour f m0) = do
     f' <- ppSCode f
-    let m' = vsep (map (PP.list . map pretty) m)
+    let m' = PP.vsep (map (PP.list . map pretty) m)
     return $
-      pretty ("Recursive behaviour of " :: Text) <> f' <> colon <> line
+      pretty ("Recursive behaviour of" :: Text) <+> f' <> colon <> line
         <> indent 2 (align m')
     where
       m = toList (HashSet.fromList m0)
diff --git a/src/MiniJuvix/Termination/CallMap.hs b/src/MiniJuvix/Termination/CallMap.hs
index b5b4cea12..7dbd732d1 100644
--- a/src/MiniJuvix/Termination/CallMap.hs
+++ b/src/MiniJuvix/Termination/CallMap.hs
@@ -6,6 +6,7 @@ where
 
 import Data.HashMap.Strict qualified as HashMap
 import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Abstract.InfoTable
 import MiniJuvix.Syntax.Abstract.Language.Extra
 import MiniJuvix.Syntax.Concrete.Scoped.Name (unqualifiedSymbol)
 import MiniJuvix.Termination.Types
@@ -22,7 +23,7 @@ viewCall ::
   Members '[Reader SizeInfo] r =>
   Expression ->
   Sem r (Maybe FunCall)
-viewCall e = case e of
+viewCall = \case
   ExpressionApplication (Application f x) -> do
     c <- viewCall f
     x' <- callArg
@@ -37,7 +38,7 @@ viewCall e = case e of
           lessThan :: Sem r CallRow
           lessThan = case x of
             ExpressionIden (IdenVar v) -> do
-              s <- asks (HashMap.lookup v . _sizeSmaller)
+              s :: Maybe Int <- asks (HashMap.lookup v . _sizeSmaller)
               return $ case s of
                 Nothing -> CallRow Nothing
                 Just s' -> CallRow (Just (s', RLe))
@@ -61,13 +62,21 @@ viewCall e = case e of
 addCall :: FunctionRef -> FunCall -> CallMap -> CallMap
 addCall fun c = over callMap (HashMap.alter (Just . insertCall c) fun)
   where
-    insertCall :: FunCall -> Maybe (HashMap FunctionRef [FunCall]) -> HashMap FunctionRef [FunCall]
-    insertCall f m = case m of
+    insertCall ::
+      FunCall ->
+      Maybe (HashMap FunctionRef [FunCall]) ->
+      HashMap FunctionRef [FunCall]
+    insertCall f = \case
       Nothing -> singl f
       Just m' -> addFunCall f m'
+
     singl :: FunCall -> HashMap FunctionRef [FunCall]
     singl f = HashMap.singleton (f ^. callRef) [f]
-    addFunCall :: FunCall -> HashMap FunctionRef [FunCall] -> HashMap FunctionRef [FunCall]
+
+    addFunCall ::
+      FunCall ->
+      HashMap FunctionRef [FunCall] ->
+      HashMap FunctionRef [FunCall]
     addFunCall fc = HashMap.insertWith (flip (<>)) (fc ^. callRef) [fc]
 
 registerCall ::
@@ -78,13 +87,16 @@ registerCall c = do
   fun <- ask
   modify (addCall fun c)
 
-buildCallMap :: TopModule -> CallMap
-buildCallMap = run . execState mempty . checkModule
+buildCallMap :: InfoTable -> TopModule -> CallMap
+buildCallMap infotable = run . execState mempty . runReader infotable . checkModule
 
-checkModule :: Members '[State CallMap] r => TopModule -> Sem r ()
+checkModule ::
+  Members '[State CallMap, Reader InfoTable] r =>
+  TopModule ->
+  Sem r ()
 checkModule m = checkModuleBody (m ^. moduleBody)
 
-checkModuleBody :: Members '[State CallMap] r => ModuleBody -> Sem r ()
+checkModuleBody :: Members '[State CallMap, Reader InfoTable] r => ModuleBody -> Sem r ()
 checkModuleBody body = do
   mapM_ checkFunctionDef moduleFunctions
   mapM_ checkLocalModule moduleLocalModules
@@ -92,15 +104,22 @@ checkModuleBody body = do
     moduleFunctions = [f | StatementFunction f <- body ^. moduleStatements]
     moduleLocalModules = [f | StatementLocalModule f <- body ^. moduleStatements]
 
-checkLocalModule :: Members '[State CallMap] r => LocalModule -> Sem r ()
+checkLocalModule :: Members '[State CallMap, Reader InfoTable] r => LocalModule -> Sem r ()
 checkLocalModule m = checkModuleBody (m ^. moduleBody)
 
-checkFunctionDef :: Members '[State CallMap] r => FunctionDef -> Sem r ()
-checkFunctionDef def = runReader (FunctionRef (unqualifiedSymbol (def ^. funDefName))) $ do
-  checkTypeSignature (def ^. funDefTypeSig)
-  mapM_ checkFunctionClause (def ^. funDefClauses)
+checkFunctionDef ::
+  Members '[State CallMap, Reader InfoTable] r =>
+  FunctionDef ->
+  Sem r ()
+checkFunctionDef FunctionDef {..} =
+  runReader (FunctionRef (unqualifiedSymbol _funDefName)) $ do
+    checkTypeSignature _funDefTypeSig
+    mapM_ checkFunctionClause _funDefClauses
 
-checkTypeSignature :: Members '[State CallMap, Reader FunctionRef] r => Expression -> Sem r ()
+checkTypeSignature ::
+  Members '[State CallMap, Reader FunctionRef, Reader InfoTable] r =>
+  Expression ->
+  Sem r ()
 checkTypeSignature = runReader (emptySizeInfo :: SizeInfo) . checkExpression
 
 emptySizeInfo :: SizeInfo
@@ -120,29 +139,39 @@ mkSizeInfo ps = SizeInfo {..}
         ]
 
 checkFunctionClause ::
-  Members '[State CallMap, Reader FunctionRef] r =>
+  Members '[State CallMap, Reader FunctionRef, Reader InfoTable] r =>
   FunctionClause ->
   Sem r ()
-checkFunctionClause cl =
-  runReader (mkSizeInfo (cl ^. clausePatterns)) $
-    checkExpression (cl ^. clauseBody)
+checkFunctionClause FunctionClause {..} =
+  runReader (mkSizeInfo _clausePatterns) $ checkExpression _clauseBody
 
-checkExpression :: Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r => Expression -> Sem r ()
-checkExpression e = do
-  mc <- viewCall e
-  case mc of
+checkExpression ::
+  Members '[State CallMap, Reader FunctionRef, Reader InfoTable, Reader SizeInfo] r =>
+  Expression ->
+  Sem r ()
+checkExpression e =
+  viewCall e >>= \case
     Just c -> do
-      registerCall c
-      mapM_ (checkExpression . snd) (c ^. callArgs)
+      h <- asks _infoFunctions
+      let fname = c ^. callRef
+          info = HashMap.lookupDefault impossible fname h
+          markedTerminating = info ^. (functionInfoDef . funDefTerminating)
+      if
+          | markedTerminating -> do
+              let cargs = map (\x -> (CallRow (Just (0, RLe)), snd x)) (c ^. callArgs)
+              registerCall $ FunCall fname cargs
+          | otherwise -> do
+              registerCall c
+              mapM_ (checkExpression . snd) (c ^. callArgs)
     Nothing -> case e of
       ExpressionApplication a -> checkApplication a
+      ExpressionFunction f -> checkFunction f
       ExpressionIden {} -> return ()
       ExpressionUniverse {} -> return ()
-      ExpressionFunction f -> checkFunction f
       ExpressionLiteral {} -> return ()
 
 checkApplication ::
-  Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r =>
+  Members '[State CallMap, Reader FunctionRef, Reader InfoTable, Reader SizeInfo] r =>
   Application ->
   Sem r ()
 checkApplication (Application l r) = do
@@ -150,7 +179,7 @@ checkApplication (Application l r) = do
   checkExpression r
 
 checkFunction ::
-  Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r =>
+  Members '[State CallMap, Reader FunctionRef, Reader InfoTable, Reader SizeInfo] r =>
   Function ->
   Sem r ()
 checkFunction (Function l r) = do
@@ -158,7 +187,7 @@ checkFunction (Function l r) = do
   checkExpression r
 
 checkFunctionParameter ::
-  Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r =>
+  Members '[State CallMap, Reader FunctionRef, Reader InfoTable, Reader SizeInfo] r =>
   FunctionParameter ->
   Sem r ()
 checkFunctionParameter p = checkExpression (p ^. paramType)
diff --git a/src/MiniJuvix/Termination/Types.hs b/src/MiniJuvix/Termination/Types.hs
index ad5057502..c24d3817c 100644
--- a/src/MiniJuvix/Termination/Types.hs
+++ b/src/MiniJuvix/Termination/Types.hs
@@ -44,8 +44,24 @@ newtype LexOrder = LexOrder (NonEmpty Int)
 makeLenses ''FunCall
 makeLenses ''CallMap
 
+filterCallMap :: Foldable f => f Text -> CallMap -> CallMap
+filterCallMap funNames =
+  over
+    callMap
+    ( HashMap.filterWithKey
+        ( \k _ ->
+            S.symbolText
+              (nameUnqualify (k ^. functionRefName))
+              `elem` funNames
+        )
+    )
+
 instance PrettyCode FunCall where
-  ppCode :: forall r. Members '[Reader Options] r => FunCall -> Sem r (Doc Ann)
+  ppCode ::
+    forall r.
+    Members '[Reader Options] r =>
+    FunCall ->
+    Sem r (Doc Ann)
   ppCode (FunCall f args) = do
     args' <- mapM ppArg args
     f' <- ppCode f
@@ -71,26 +87,21 @@ instance PrettyCode FunCall where
       dbrackets x = pretty '⟦' <> x <> pretty '⟧'
 
 instance PrettyCode CallMap where
-  ppCode :: forall r. Members '[Reader Options] r => CallMap -> Sem r (Doc Ann)
+  ppCode ::
+    forall r.
+    Members '[Reader Options] r =>
+    CallMap ->
+    Sem r (Doc Ann)
   ppCode (CallMap m) = vsep <$> mapM ppEntry (HashMap.toList m)
     where
       ppEntry :: (A.FunctionRef, HashMap A.FunctionRef [FunCall]) -> Sem r (Doc Ann)
       ppEntry (fun, mcalls) = do
         fun' <- annotate AnnImportant <$> ppCode fun
         calls' <- vsep <$> mapM ppCode calls
-        return $ fun' <+> waveFun <+> align calls'
+        return $ fun' <+> kwWaveArrow <+> align calls'
         where
           calls = concat (HashMap.elems mcalls)
 
-kwQuestion :: Doc Ann
-kwQuestion = annotate AnnKeyword "?"
-
-waveFun :: Doc ann
-waveFun = pretty ("↝" :: Text)
-
-vsep2 :: [Doc ann] -> Doc ann
-vsep2 = concatWith (\a b -> a <> line <> line <> b)
-
 instance PrettyCode CallRow where
   ppCode (CallRow r) = return $ case r of
     Nothing -> kwQuestion
@@ -99,6 +110,3 @@ instance PrettyCode CallRow where
 
 instance PrettyCode CallMatrix where
   ppCode l = vsep <$> mapM ppCode l
-
-filterCallMap :: Foldable f => f Text -> CallMap -> CallMap
-filterCallMap funNames = over callMap (HashMap.filterWithKey (\k _ -> S.symbolText (nameUnqualify (k ^. functionRefName)) `elem` funNames))
diff --git a/src/MiniJuvix/Termination/Types/SizeRelation.hs b/src/MiniJuvix/Termination/Types/SizeRelation.hs
index 01c190060..882f9d44b 100644
--- a/src/MiniJuvix/Termination/Types/SizeRelation.hs
+++ b/src/MiniJuvix/Termination/Types/SizeRelation.hs
@@ -1,13 +1,9 @@
 module MiniJuvix.Termination.Types.SizeRelation where
 
---------------------------------------------------------------------------------
-
 import Data.Semiring
 import MiniJuvix.Prelude
 import Prettyprinter
 
---------------------------------------------------------------------------------
-
 data Rel
   = RJust Rel'
   | RNothing
diff --git a/src/MiniJuvix/Translation/ScopedToAbstract.hs b/src/MiniJuvix/Translation/ScopedToAbstract.hs
index 8d02aecf2..1ed4eb4b8 100644
--- a/src/MiniJuvix/Translation/ScopedToAbstract.hs
+++ b/src/MiniJuvix/Translation/ScopedToAbstract.hs
@@ -29,16 +29,22 @@ entryAbstract _resultScoper = do
   where
     ms = _resultScoper ^. Scoper.resultModules
 
--- translateModule :: Module 'Scoped 'ModuleTop -> Either Err (InfoTable, A.TopModule)
--- translateModule = run . runError . runInfoTableBuilder . goTopModule
-
-goTopModule :: Members '[Error Err, InfoTableBuilder] r => Module 'Scoped 'ModuleTop -> Sem r A.TopModule
+goTopModule ::
+  Members '[Error Err, InfoTableBuilder] r =>
+  Module 'Scoped 'ModuleTop ->
+  Sem r A.TopModule
 goTopModule = goModule
 
-goLocalModule :: Members '[Error Err, InfoTableBuilder] r => Module 'Scoped 'ModuleLocal -> Sem r A.LocalModule
+goLocalModule ::
+  Members '[Error Err, InfoTableBuilder] r =>
+  Module 'Scoped 'ModuleLocal ->
+  Sem r A.LocalModule
 goLocalModule = goModule
 
-goModule :: (Members '[Error Err, InfoTableBuilder] r, ModulePathType 'Scoped t ~ S.Name' c) => Module 'Scoped t -> Sem r (A.Module c)
+goModule ::
+  (Members '[Error Err, InfoTableBuilder] r, ModulePathType 'Scoped t ~ S.Name' c) =>
+  Module 'Scoped t ->
+  Sem r (A.Module c)
 goModule (Module n par b) = case par of
   [] -> A.Module n <$> goModuleBody b
   _ -> unsupported "Module parameters"
@@ -62,6 +68,7 @@ goModuleBody ss' = do
   where
     ss :: [Indexed (Statement 'Scoped)]
     ss = zipWith Indexed [0 ..] ss'
+
     compiledFunctions :: Sem r [Indexed A.FunctionDef]
     compiledFunctions =
       sequence $
@@ -105,10 +112,11 @@ goFunctionDef ::
   TypeSignature 'Scoped ->
   NonEmpty (FunctionClause 'Scoped) ->
   Sem r A.FunctionDef
-goFunctionDef sig clauses = do
-  let _funDefName = sig ^. sigName
+goFunctionDef TypeSignature {..} clauses = do
+  let _funDefName = _sigName
+      _funDefTerminating = _sigTerminating
   _funDefClauses <- mapM goFunctionClause clauses
-  _funDefTypeSig <- goExpression (sig ^. sigType)
+  _funDefTypeSig <- goExpression _sigType
   registerFunction' A.FunctionDef {..}
 
 goFunctionClause ::
@@ -173,14 +181,15 @@ goConstructorDef ::
   Members '[Error Err] r =>
   InductiveConstructorDef 'Scoped ->
   Sem r A.InductiveConstructorDef
-goConstructorDef (InductiveConstructorDef c ty) = A.InductiveConstructorDef c <$> goExpression ty
+goConstructorDef (InductiveConstructorDef c ty) =
+  A.InductiveConstructorDef c <$> goExpression ty
 
 goExpression ::
   forall r.
   Members '[Error Err] r =>
   Expression ->
   Sem r A.Expression
-goExpression e = case e of
+goExpression = \case
   ExpressionIdentifier nt -> return (goIden nt)
   ExpressionParensIdentifier nt -> return (goIden nt)
   ExpressionApplication a -> A.ExpressionApplication <$> goApplication a
@@ -251,17 +260,26 @@ goPatternApplication ::
   Sem r A.ConstructorApp
 goPatternApplication a = uncurry A.ConstructorApp <$> viewApp (PatternApplication a)
 
-goPatternConstructor :: forall r. Members '[Error Err] r => ConstructorRef -> Sem r A.ConstructorApp
+goPatternConstructor ::
+  Members '[Error Err] r =>
+  ConstructorRef ->
+  Sem r A.ConstructorApp
 goPatternConstructor a = uncurry A.ConstructorApp <$> viewApp (PatternConstructor a)
 
-goInfixPatternApplication :: forall r. Members '[Error Err] r => PatternInfixApp -> Sem r A.ConstructorApp
+goInfixPatternApplication ::
+  Members '[Error Err] r =>
+  PatternInfixApp ->
+  Sem r A.ConstructorApp
 goInfixPatternApplication a = uncurry A.ConstructorApp <$> viewApp (PatternInfixApplication a)
 
-goPostfixPatternApplication :: forall r. Members '[Error Err] r => PatternPostfixApp -> Sem r A.ConstructorApp
+goPostfixPatternApplication ::
+  Members '[Error Err] r =>
+  PatternPostfixApp ->
+  Sem r A.ConstructorApp
 goPostfixPatternApplication a = uncurry A.ConstructorApp <$> viewApp (PatternPostfixApplication a)
 
 viewApp :: forall r. Members '[Error Err] r => Pattern -> Sem r (A.ConstructorRef, [A.Pattern])
-viewApp p = case p of
+viewApp = \case
   PatternConstructor c -> return (goConstructorRef c, [])
   PatternApplication (PatternApp l r) -> do
     r' <- goPattern r
@@ -283,7 +301,7 @@ viewApp p = case p of
 goConstructorRef :: ConstructorRef -> A.ConstructorRef
 goConstructorRef (ConstructorRef' n) = A.ConstructorRef n
 
-goPattern :: forall r. Members '[Error Err] r => Pattern -> Sem r A.Pattern
+goPattern :: Members '[Error Err] r => Pattern -> Sem r A.Pattern
 goPattern p = case p of
   PatternVariable a -> return $ A.PatternVariable a
   PatternConstructor c -> A.PatternConstructorApp <$> goPatternConstructor c
diff --git a/src/MiniJuvix/Utils/Version.hs b/src/MiniJuvix/Utils/Version.hs
index 0658f75b7..a74ad03d4 100644
--- a/src/MiniJuvix/Utils/Version.hs
+++ b/src/MiniJuvix/Utils/Version.hs
@@ -13,8 +13,6 @@ module MiniJuvix.Utils.Version
   )
 where
 
-------------------------------------------------------------------------------
-
 import Data.Version (showVersion)
 import Development.GitRev (gitBranch, gitCommitDate, gitHash)
 import MiniJuvix.Prelude hiding (Doc)
@@ -23,8 +21,6 @@ import Prettyprinter as PP
 import Prettyprinter.Render.Text (renderIO)
 import System.Environment (getProgName)
 
-------------------------------------------------------------------------------
-
 versionDoc :: Doc Text
 versionDoc = PP.pretty (showVersion Paths_minijuvix.version)
 
diff --git a/tests/negative/Termination/Loop.mjuvix b/tests/negative/Termination/Loop.mjuvix
new file mode 100644
index 000000000..f445ef947
--- /dev/null
+++ b/tests/negative/Termination/Loop.mjuvix
@@ -0,0 +1,11 @@
+module NoLexOrde;
+
+axiom A : Type;
+
+f : A -> A -> A;
+g : A -> A -> A;
+
+g x y := f x x;
+f x y := g x (f x x);
+
+end;
diff --git a/tests/negative/Termination/ToEmpty.mjuvix b/tests/negative/Termination/ToEmpty.mjuvix
new file mode 100644
index 000000000..6bafb113e
--- /dev/null
+++ b/tests/negative/Termination/ToEmpty.mjuvix
@@ -0,0 +1,6 @@
+module ToEmpty;
+  axiom A : Type;
+  inductive Empty {};
+  f : A -> Empty;
+  f x := f x;
+end;
diff --git a/tests/positive/Termination/TerminatingF.mjuvix b/tests/positive/Termination/TerminatingF.mjuvix
new file mode 100644
index 000000000..4a533abf4
--- /dev/null
+++ b/tests/positive/Termination/TerminatingF.mjuvix
@@ -0,0 +1,13 @@
+module TerminatingF;
+
+axiom A : Type;
+
+terminating
+f : A -> A -> A;
+
+g : A -> A -> A;
+
+g x y := f x x;
+f x y := g x (f x x);
+
+end;
diff --git a/tests/positive/Termination/TerminatingG.mjuvix b/tests/positive/Termination/TerminatingG.mjuvix
new file mode 100644
index 000000000..1994489e2
--- /dev/null
+++ b/tests/positive/Termination/TerminatingG.mjuvix
@@ -0,0 +1,13 @@
+module TerminatingG;
+
+axiom A : Type;
+
+f : A -> A -> A;
+
+terminating
+g : A -> A -> A;
+
+g x y := f x x;
+f x y := g x (f x x);
+
+end;
diff --git a/tests/positive/Termination/ToEmpty.mjuvix b/tests/positive/Termination/ToEmpty.mjuvix
new file mode 100644
index 000000000..4d00971a1
--- /dev/null
+++ b/tests/positive/Termination/ToEmpty.mjuvix
@@ -0,0 +1,7 @@
+module ToEmpty;
+  axiom A : Type;
+  inductive Empty {};
+  terminating
+  f : A -> Empty;
+  f x := f x;
+end;