Email Gateway (Aug 19 2022 at 13:11): Email Gateway (Aug 19 2022 at 13:11):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
when I tried to adapt Isabelle/HOLCF Prelude (e.g.,
hg clone http://hg.code.sf.net/p/holcf-prelude/code holcf-prelude
) to Isabelle2013-2-RC3 I got an exception in the definition of
fixrec scanr :: "('a → 'b → 'b) → 'b → ['a] → ['b]" where
"scanr⋅f⋅q0⋅[] = [q0]" |
"scanr⋅f⋅q0⋅(x : xs) = (
let qs = scanr⋅f⋅q0⋅xs in
(case qs of
[] ⇒ ⊥
| q : _ ⇒ f⋅x⋅q : qs))"
(and similar definitions). The error message is
exception TERM raised (line 142 of "Syntax/syntax_trans.ML"):
binder_tr: _cabs
\<^const>dummy_pattern
\<^const>Cfun.Rep_cfun (\<^const>Cfun.Rep_cfun
\<^const>Data_List.list.Cons (\<^const>Cfun.Rep_cfun
(\<^const>Cfun.Rep_cfun f x) q)) qs
What is this supposed to tell me? ;)
cheers
chris
Email Gateway (Aug 19 2022 at 13:15):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Good question. Maybe it is related to recent renovations in the case
syntax!? Any experts in this and/or HOLCF?
Florian
signature.asc
Email Gateway (Aug 19 2022 at 13:15):From: Dmitriy Traytel <traytel@in.tum.de>
The recent renovations of the case syntax are not used in HOLCF. There
was a thread on this earlier (which didn't lead to any reasonable code
changes AFAIK):
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-April/004067.html
Dmitriy
Last updated: Nov 21 2024 at 12:39 UTC