[Agda] Hanging out with the Lean crowd

[Ettore Aldrovandi]

Hi James, 

mathematician lurker here.  This is interesting:

> On Aug 21, 2020, at 12:47, James Wood <james.wood.100 at strath.ac.uk> wrote:
> 
> Most other areas of maths traditionally don't resemble this
> type-directed style of programming. There are few, small, inductive
> types, and a lot of reasoning is done at the level of algebraic axioms
> (with no inductive types in sight). These features largely nullify
> Agda's advantages, and instead the advantages of Lean and Coq in the
> field of proving shine through.

Can you elaborate a bit?

Thanks,

—Ettore
Ettore Aldrovandi
Department of Mathematics, Florida State University
1017 Academic Way                *   http://www.math.fsu.edu/~ealdrov
Tallahassee, FL 32306-4510, USA * * aldrovandi at math dot fsu dot edu

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200821/82fe7ac6/attachment.html>