Ticks for Basics
  max-open-constraints = 0
  pointers = 0
  pointers (reused) = 0
  max-open-metas = 1
  unequal terms = 2
  metas = 13
  equal terms = 23
Ticks for Pr
  max-open-constraints = 0
  pointers = 0
  pointers (reused) = 0
  max-open-metas = 3
  unequal terms = 17
  metas = 88
  equal terms = 172
Ticks for Nom
  pointers = 0
  pointers (reused) = 0
  max-open-constraints = 2
  max-open-metas = 4
  attempted-constraints = 8
  unequal terms = 75
  metas = 87
  equal terms = 216
Ticks for Kind
  max-open-constraints = 0
  pointers = 0
  pointers (reused) = 0
  max-open-metas = 1
  metas = 10
  equal terms = 20
Ticks for Cxt
  max-open-constraints = 0
  pointers = 0
  pointers (reused) = 0
  max-open-metas = 1
  unequal terms = 5
  metas = 59
  equal terms = 190
Ticks for Loc
  max-open-constraints = 0
  pointers = 0
  pointers (reused) = 0
  max-open-metas = 6
  metas = 145
  unequal terms = 145
  equal terms = 335
Ticks for Term
  pointers = 0
  pointers (reused) = 0
  max-open-constraints = 2
  attempted-constraints = 4
  max-open-metas = 10
  unequal terms = 158
  metas = 241
  equal terms = 615
Ticks for Shift
  pointers = 0
  pointers (reused) = 0
  max-open-constraints = 2
  max-open-metas = 14
  attempted-constraints = 16
  metas = 230
  unequal terms = 411
  equal terms = 633
Ticks for Eta
  pointers = 0
  pointers (reused) = 0
  max-open-constraints = 2
  attempted-constraints = 12
  max-open-metas = 18
  metas = 185
  unequal terms = 270
  equal terms = 487
Ticks for Inst
  pointers = 0
  pointers (reused) = 0
  max-open-constraints = 2
  attempted-constraints = 9
  max-open-metas = 16
  metas = 276
  unequal terms = 534
  equal terms = 948
Ticks for Subst
  pointers = 0
  pointers (reused) = 0
  max-open-constraints = 2
  attempted-constraints = 8
  max-open-metas = 13
  metas = 202
  unequal terms = 315
  equal terms = 576
Ticks for Syntacticosmos
  max-open-constraints = 0
  pointers = 0
  pointers (reused) = 0
  max-open-metas = 1
  metas = 1
  equal terms = 21
Ticks for UntypedLambda
  pointers = 0
  pointers (reused) = 0
  max-open-constraints = 2
  attempted-constraints = 20
  max-open-metas = 23
  metas = 101
  unequal terms = 124
  equal terms = 180
agda -v0 -v profile:100 Syntacticosmos/UntypedLambda.agda --ignore-interfaces -iSyntacticosmos +RTS -K32M -slogs/.tmp 
   2,979,201,920 bytes allocated in the heap
     747,827,064 bytes copied during GC
      26,543,392 bytes maximum residency (39 sample(s))
         838,256 bytes maximum slop
              75 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      5678 colls,     0 par    1.09s    1.10s     0.0002s    0.0011s
  Gen  1        39 colls,     0 par    0.81s    0.81s     0.0209s    0.0714s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time    3.10s  (  3.14s elapsed)
  GC      time    1.91s  (  1.91s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time    5.01s  (  5.05s elapsed)

  %GC     time      38.1%  (37.8% elapsed)

  Alloc rate    959,752,876 bytes per MUT second

  Productivity  61.9% of total user, 61.5% of total elapsed

──────────────────────────────────────────────────────────────────
No info
