Core.Termination.SizeChange

Definitions

CallSeq : Type

  A sequence in the call graph lists the source location of the successive
  calls and the name of each of the functions being called
  TODO: also record the arguments so that we can print e.g.
    flip x y -> flop y x -> flip x y
  instead of the less useful
    flip -> flop -> flip

Visibility: public export

calcTerminating : Ref Ctxt Defs => FC -> Name -> Core Terminating

Visibility: export