TC.Rules.Def.checkclause reached A.WithRHS
DebugWith.with-34 (f b)
with function module: [DebugWith] free variables: 0
delta  = (trash1 : Trash) (b : A) (trash2 : Trash)
         (f : (x : A) → P x) (trash3 : Trash)
vs     = [f b]
as     = [P b]
perm   = x0,x1,x2,x3,x4 -> x0,x1,x2,x3,x4
delta1 = (b : A) (f : (x : A) → P x)
delta2 = (trash1 : Trash) (trash2 : Trash) (trash3 : Trash)
perm'  = x0,x1,x2,x3,x4 -> x1,x3,x0,x2,x4
fPerm  = x0,x1,x2,x3,x4 -> x1,x3,x0,x2,x4
    with arguments [f b]
             types [P b]
with function call DebugWith.with-34 b f (f b) trash1 trash2 trash3
           context (trash4 : Trash) (b₁ : A) (trash5 : Trash)
                   (f₁ : (x : A) → P x) (trash6 : Trash)
             delta (trash1 : Trash) (b : A) (trash2 : Trash)
                   (f : (x : A) → P x) (trash3 : Trash)
            delta1 (b : A) (f : (x : A) → P x)
            delta2 (trash1 : Trash) (trash2 : Trash)
                   (trash3 : Trash)
              body DebugWith.with-34 b f (f b) trash1 trash2 trash3
checkWithFunction
  delta1 = (b : A) (f : (x : A) → P x)
  delta2 = (trash1 : Trash) (trash2 : Trash) (trash3 : Trash)
  t      = Trash → A → Trash → ((x : A) → P x) → Trash → Set
  as     = [P b]
  vs     = [f b]
  b      = Set
  qs     = [trash1, b, trash2, f, trash3]
  perm'  = x0,x1,x2,x3,x4 -> x1,x3,x0,x2,x4
  perm   = x0,x1,x2,x3,x4 -> x0,x1,x2,x3,x4
  fperm  = x0,x1,x2,x3,x4 -> x1,x3,x0,x2,x4
  withSub= Var 0 [] :# (Var 4 [] :# (Var 1 [] :# (Var 5 [] :# (Var 2 [] :# Wk 6 IdS))))
created with display form
Display 6 [$ @0, $ @0, $ @0, $ @0, $ @0, $ @0]
        test @2 @5 @1 @4 @0 | @3
added with function DebugWith.with-34 of type
  (b : A) (f : (x : A) → P x) →
  P b → (trash1 trash2 trash3 : Trash) → Set
  -|
DebugWith.agda:15,11-23
Trash !=< Set of type Set
when checking that the expression provokeError has type Set
