[Agda] I want implicit coercions in Agda

[Apostolis Xekoukoulotakis]

Is there a way to inspect a term in the context of a function? To find its
type and the type of the variables it depends on?
It seems that all you can do is be directed to the definition of a function
and nothing more.

Holes are very useful when you write a proof. As soon as you have written
the proof , you lose all information about it except from what you can see
in the text.
So here is an oxymoron. It is easier to write proofs than to understand
already written ones.
I too believe that the future is the use of interactive tools to inspect
the code.

As far as replacing hand written proofs all together , I am not so sure it
is possible. I hope that one day we get there , though.

On Sat, Nov 17, 2018 at 8:14 PM Sergei Meshveliani <mechvel at botik.ru> wrote:

> On Sat, 2018-11-17 at 16:54 +0000, Peter Hancock wrote:
> > On 17/11/2018 15:53, Martin Escardo wrote:
> > > If you want mathematicians to use proof assistants, you have to
> > > implement the notations they use, not the notations that computer
> > > scientists / engineers find convenient to write computer programs.
> > > Martin
> >
> > You might as well say that if you want mathematicians to use
> > type-setting software you have to implement the notations they use.
> > The mathematicians I know seem to find their way pretty well around
> LaTeX, etc,
> > for all its barbarity.
> >
> > Perhaps one can think of mathematical notation as a matter of DSLs.
> > LaTeX is full of DSL-like apparatus for things like category theory
> diagrams, etc.
> > I think the support in Agda for equational reasoning might be
> > a nice example of a DSL.
> >
> > Is there a general definition of coercion?  Is there a connection with
> identity types?
> >
> > [..]
>
> Coercion has not sense in general.
> But mathematicians (S.Lang and Van der Waerden, and many others) write
> that a group homomorphism is a map f that satisfies
> the equality
>                                f(xy) = f(x)f(y),
>
> that a ring homomorphism needs to satisfy
>
>                                f(x+y) = f(x) + f(y),
> and so on.
> These books write so, because this way it is easier to explain and to
> understand. This has been tested by thousands of professors and millions
> of students.
>
> Generally, compilers are forced to follow science (mathematics).
>
> * For example, in early days programs used numbers instead of names.
> Then they have improved.
> * They used different functions to add polynomials over integers,
> to add polynomials over rationals, over polynomial, and so on.
> Then, they have improved, and introduced generic programming -- this
> follows mathematics.
> * In mathematics, domains depend on a value, and this value can be
> computed dynamically, and a function can return a domain.
> Compilers could not handle this.
> But they have improved, and now they can.
>
> * Similar it is (or will be) with implicit conversion.
>
> Science has more sense than programming, science is wiser than a
> technology, it is fundamental. And programming has to follow science.
>
> Regards,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181117/70cbac60/attachment.html>