Stream: Beginner Questions

Topic: instantiation


view this post on Zulip 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?

view this post on Zulip Mathias Fleury (May 27 2021 at 15:21):

most likely you forgot some more parameters

view this post on Zulip 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

view this post on Zulip Mathias Fleury (May 27 2021 at 15:23):

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

view this post on Zulip Mathias Fleury (May 27 2021 at 15:30):

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

view this post on Zulip 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?

view this post on Zulip 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: Sep 25 2021 at 09:17 UTC