zibo yang (May 27 2021 at 14:45): zibo yang (May 27 2021 at 14:45):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?
Mathias Fleury (May 27 2021 at 15:21):most likely you forgot some more parameters
Mathias Fleury (May 27 2021 at 15:23):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)
Mathias Fleury (May 27 2021 at 15:30):and in the goal the non-instantiated arguments are written in blue
Jakub Kądziołka (May 27 2021 at 15:32):Does infinite_coin_toss_space (or its parent locales) use any fixes you'd need to provide values for?
Manuel Eberl (May 27 2021 at 15:40):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: Dec 21 2024 at 16:20 UTC