On 30/10/2020 17:29, Ralf Hemmecke wrote:
> In FriCAS they are not (also not in Aldor).
> The reason is that no computation is done at compile time.
> Of course that could be changed if there were a sublanguage that the
> compiler could execute at compile time.
>
> But why would you believe that 3 is the same as 1 + 2? I can surely
> program NonNegativeInteger in such a way that 1+2 gives 6 (or perhaps
> 0). Would you then also claim that the type of a and b are the same?
Yes, that is the reason that Idris has a proof system built into the
language, it is completely separate from language constructs like:
if 1+2=3 then ...
where the user can define equality in different ways.
Instead it uses Martin-Löf equality types which only has one
constructor: Refl.
Martin
--
You received this message because you are subscribed to the Google Groups "FriCAS -
computer algebra system" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to fricas-devel+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/fricas-devel/116f4a2d-e8b3-200a-c761-ad485b4d2def%40martinb.com.
