Re: [isabelle] Failing simproc



> $ zgrep 'IGNORED result of simproc' * | cut -d\" -f2 | sort | uniq -c
>      86 equal

I'm wondering a little bit about this.  The simproc »equal« is part of
the code generatorm, preprocessor, as follows:

setup {*
  Code_Preproc.map_pre (fn simpset =>
    simpset addsimprocs [Simplifier.simproc_global_i @{theory} "equal"
[ at {term HOL.eq}]
      (fn thy => fn _ =>
        fn Const (_, Type ("fun", [Type _, _])) => SOME @{thm eq_equal}
| _ => NONE)])
*}

I don't see any instantiation of schematic variables here, but I'm more
or less ignorant about the simproc business, so the code above may be
utterly wrong or conceptionally outdated.

	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.