Re: [isabelle] Definition of fact



For functions like 'fact' and 'exp' it is possible to define it in the
locale of the type class. Here it is welcomed to change.

Unfortunately, for has_derivative this is not possible, as it is defined
between two types.

 - Johannes

Am Samstag, den 31.10.2015, 19:42 +0100 schrieb Manuel Eberl:
> I noticed that âfactâ (the factorail function) is defined as
> 
> fun fact :: "nat â ('a::semiring_char_0)"
> 
> as opposed to
> 
> fun (in semiring_char_0) fact :: "nat â 'a"
>    where "fact 0 = 1" | "fact (Suc n) = of_nat (Suc n) * fact n"
> 
> There are similar issues with some other constants like exp and 
> has_derivative that make it impossible to use fact/exp/has_derivative 
> etc. inside type class assumptions.
> 
> 
> Is there an actual reason for this? If not, I think this should be changed.
> 
> 
> Cheers,
> 
> Manuel
> 
> 
> 
> 






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