{ let rec
  { Fact = -- compile-time constant binding
    { proc { N } as -- precondition: N.IsI48[] & (N >= 0)
      { if N == 0 then 1 else
        N * Fact[N - 1]
      }
    }
  }
  in -- use Fact here or just make the whole expression to evaluate to it:
  Fact
}