[Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq

[Dan Doel]

On Tue, Jan 7, 2014 at 2:43 PM, Maxime Dénès <mail at maximedenes.fr> wrote:
> In fact, I was wondering why the call to subst (which is defined by
> pattern matching) destroys the proper subterm status, while it is not
> the case for pattern matching. It does not seem very uniform, does it?
>
> In Coq, a reduction step would replace subst by its body before
> computing the size information.

It is not possible to replace subst by its body in Agda. Function
definition by dependent pattern matching is taken to be primitive, so
there is no expression that can be said to be its body.

Even the 'with' syntax, which you could use to perform the same
operation without defining subst is taken to be sugar for an auxiliary
function definition.

Uniformity with respect to inlining is not really something that
Agda's (non-sized-type) termination checker is strong at, though.

-- Dan