Re: [isabelle] Failing simproc



>> 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)])
>> *}
> 
> Are there situations where this rewrite step is expected to fail (maybe
> due to sort constraints)? Then this warning would be expected, too.

Failure is expected due to types themselves: only instantiated equality
(eq [tyco …]) is rewritten, not fully polymorphic equality (eq ['a]).

	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.