Re: [isabelle] exception using "case ... of ..." with HOLCF



> 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? ;)

Good question.  Maybe it is related to recent renovations in the case
syntax!?  Any experts in this and/or HOLCF?

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.