I am trying to define a recursive function, but for some reason I get an error:
exception TERM raised (line 272 of "~~/src/HOL/Tools/hologic.ML"): dest_eq |supp id| <o |UNIV|
the function in question is this:
function f :: "'a::var_τ_pre raw_τ ⇒ 'a ssfun ⇒ 'a τ" where "f (raw_τ_ctor x) p = CTOR (map_τ_pre id id (λt. (t, f t)) (λt. (t, f t)) (map_τ_pre id (pick0 x p) (rename_τ (pick0 x p)) id x)) p"
There are a few theorems that would require
|supp id| <o |UNIV| but I do not see how they would are involved here.
Might be a good idea to enable the ML stack trace to see where that exception comes from exactly.
I guess this means I need to load up this code in a pure session, because the stack traces do not work with a precompiled HOL session
ah, yes, because the function package was defined in HOL…
yeah you don't want to do this
well, you can try
it might work
I remember running into some performance issues with the whole stack trace/debugger thing, but I don't remember exactly what I was doing at the time.
I am somewhat surprised though; this looks like some sort of cardinality constraint that I would have expected to come perhaps from the datatype package, but not the function package.
Or are you doing something where this
|supp id| <o |UNIV| might be coming from?
The stuff I am working on is an extension of the datatype package. So yeah there are a few theorems like map_comp that require that, but I do not see how that is relevant for the function definition
Well, currently HOL and HOL-Cardinals is loading, so let's see where this error actually comes from
does the function package use the theorems of the datatype package?
because that might explain it. I do register my datatypes as BNFs, but there are theorems already defined of the name
<name>.map_comp that have those extra assumptions
Hm, not sure. Maybe for the pattern matching. You could try expressing the pattern matching with a
case expression and see what happens then.
using a case expression does not change this. The stack trace tells me it happens when trying to find a congruence rule. I will investigate further once it has reloaded everything because I opened the ML files
Last updated: Dec 07 2023 at 20:16 UTC