Great, is it still as easy to use as before (for instance for stating
the computation rule for loop?)
And did you check that the proof of pi_1(S^1) still works?
By the way, I disagree with the following sentence:
> [There] is not fundamental reason why the Agda implementation of
> functions defined by cases should be that different from the Coq
> implementation of pattern-matching.
As far as I know, the implementation of pattern-matching in Agda is
very different from Coq, because functions defined by pattern matching
is a primitive notion in Agda.
Pattern matching is not syntactic sugar for the use of an eliminator
or for a match construct. In Agda a function defined by pattern
matching is never desugared to a single term, it is just stored as a
sequence of clauses according to the form of the patterns and it will
only reduce to an actual term when the function is applied to an
argument matching one of the patterns. So Agda can’t notice that the
two terms are equal given that there are no terms to compare.
Just to be clear I’m not saying that it’s better (the fact that
pattern matching can be reduced to eliminators is still an open
question), it’s just different and happens to change something in this
case.
Guillaume
> --
> You received this message because you are subscribed to the Google Groups
> "IAS Univalent Foundations" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to
univalent-founda...@googlegroups.com.
> To post to this group, send email to
univalent-...@googlegroups.com.
> Visit this group at
>
http://groups.google.com/group/univalent-foundations?hl=en.
> For more options, visit
https://groups.google.com/groups/opt_out.
>
>