Stream: math-comp users

Topic: Beta-reduction of finite function


view this post on Zulip Ricardo (Nov 25 2022 at 14:24):

Hi. How does one beta-reduce an expression of the form f x where f is a finite function in a proof?

view this post on Zulip Ricardo (Nov 25 2022 at 14:33):

I tried cbn, hnf and simpl and none works.

view this post on Zulip Ricardo (Nov 25 2022 at 14:38):

I even tried with

  change ([ffun k0 => if fsval k0 \in ks
                      then v
                      else odflt v m.[? fsval k0]]
            (fincl ks_sub [` H]))
    with (if fsval (fincl ks_sub [` H]) \in ks
          then v
          else odflt v m.[? fsval (fincl ks_sub [` H])]).

and didn't work. That's suspicious.


Last updated: Feb 08 2023 at 07:02 UTC