Jonas Stahl (Sep 23 2024 at 11:46): Jonas Stahl (Sep 23 2024 at 11:46):Hello together,
I am currently using Specification.definition to register a new function definition like this:
val def = Binding.name ("T_map_def")
val eq = @{term "T_map f xs = T2_map (undefined::'a ⇒ nat,f) xs"} |> HOLogic.mk_Trueprop
val ctxt' = Specification.definition NONE [] [] ((def, []), eq) ctxt
I found on another that it's better to use Local_Theory.define, but sadly there's not really an example on registering function definitions. Can Local_Theory.define only be used for function with lambdas or is there a better solution?
val def = Binding.name ("T_map_def")
val name = Binding.name "T_map"
val rhs = @{term "(λf xs. T2_map (undefined::'a ⇒ nat,f) xs)"}
val ctxt'' = Local_Theory.define ((name, NoSyn), ((def, []), rhs)) ctxt
Last updated: Dec 21 2024 at 16:20 UTC