Hi all, I'm trying to create a function (with termination that should hopefully be proved by `fun`

's default methods) and hit a bit of a roadblock trying to understand local theories. I'm experimenting with something like this:

```
ML ‹
val a_binding = @{binding a}
;
Function_Fun.add_fun
[(a_binding, NONE, NoSyn)]
[
(((a_binding, []), @{term "HOL.Trueprop (a n = 3)"})
, []
, [])
]
Function_Fun.fun_config
@{context}
›
```

This leads to a "Missing local theory context" error. In general, how do I turn my `@{context}`

into a local theory context? I found the cookbook section 4.3, but it doesn't really help me understand what's going on.

```
local_setup ‹
let
val a_binding = @{binding a}
in
Function_Fun.add_fun
[(a_binding, NONE, NoSyn)]
[
(((a_binding, []), @{term "HOL.Trueprop (a n = 3)"})
, []
, [])
]
Function_Fun.fun_config
end
›
```

`add_fun`

transforms the local theory. Using local_setup, the local theory context will be passed to your function.

Last updated: Dec 07 2023 at 16:21 UTC