bridging the gap between noncomputable definitions and code

Stream: new members

[tzlil]

ive defined a certain PGame, and ive proved things about it using the grundyValue
since my game is short (always terminates) i have a decidable way to compute the value for a board
id like to use all my previous definitions which use grundyValue now but they remain noncomputable, is there a easy way to reconcile these definitions with my computable grundy value function or am i doomed to write a bunch of boilerplate whenever i use them?

[Henrik Böving]

Could you get a little more concrete? Do you have some code examples?

[tzlil]

Henrik Böving said:

Could you get a little more concrete? Do you have some code examples?

def Move.preposition {b : Board n} (m : Move b) : Board n := by
  use Board.flip <| Move.Apply Board.Initial (Move.lift m)

noncomputable def Move.xorness {b : Board n} (m : Move b) : Nimber := by
  exact grundyValue (FlippingGame (Move.preposition m))

for example this is one of the properties which are technically totally computable i just have to write a bunch of boilerplate to reconcile it with the definition of grundyValue being noncomputable
i have the actual function capable of computing

partial def grundyFast {grundyMemo : IO.Ref (Std.HashMap (Board n) ℕ)} (b : Board n) : IO ℕ

or alternatively i also have a version of this in ST
and i could if i wanted prove grundyFast b = grundyValue (FlippingGame b)
and then presumably write something like Move.xornessComputable .... and prove Move.xornessComputable = Move.xorness, i dont know what would be a good way