can someone explain to me how to instantiate locale like:

```
locale prob_grw = infinite_coin_toss_space +
fixes geom_proc::"nat ⇒ bool stream ⇒ real" and u::nat and d::nat and init::nat
assumes geometric_process:"geom_proc = gambler_rand_walk u d init"
interpretation gambler_prob_grw : prob_grw geom_proc 4 6 init
```

I want to instantiate the parameters u and d with 4 and 6, but it doesn't work like

```
No type arity fun :: numeral
```

why?

most likely you forgot some more parameters

I find that syntax easier to use and less error-prone:

```
interpretation gambler_prob_grw : prob_grw where
geom_proc = geom_proc and
u = 4 and
v = 6 and
init = init
```

(it avoids the problem of ordering of the arguments and later changing the order)

and in the goal the non-instantiated arguments are written in blue

Does `infinite_coin_toss_space`

(or its parent locales) use any `fixes`

you'd need to provide values for?

Mathias Fleury said:

I find that syntax easier to use and less error-prone:

`interpretation gambler_prob_grw : prob_grw where geom_proc = geom_proc and u = 4 and v = 6 and init = init`

🤯

Last updated: Sep 25 2022 at 23:25 UTC