I want to understand clearly affects how many steps it might take to completely proof a single goal. i.e. I want to understand the interface to the current function:

```
steps(goal,...) = # steps to prove goal
```

intuitively it must depend on the current tactic applied to `goal`

and the knowledge we have (e.g. environment & context).

Does this mean that the function has the following signature?

```
steps(goal, Tactic, Env, Context)
```

my hunch is that it actually **only** requires

```
steps(goal, Tactic)
```

since the information needed to break up the current proof obligation/goal is all in Tactic (e.g. it refers to the knowledge in the context or environment needed to correctly apply to the current goal).

Is this correct?

I guess in principle the # of steps for the current goal depends on the steps for all subsequent goalsâ€¦and those might need specific knowledge that might not be current reachable from only the tactic (i.e. we do need the current context AND the environment).

As long as a proof does NOT do random imports in the middle now I believe that:

```
steps(goal,Tactic,context,env)
```

is necessary (sorry changed my mind).

Is this correct? Whatâ€™s the right interface to that function?

Just curious what factors affect how long a proof is basically.