coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] efficiently reducing away mentions of a variable

From: Enrico Tassi <enrico.tassi AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] efficiently reducing away mentions of a variable
Date: Tue, 14 Feb 2017 14:54:14 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=enrico.tassi AT inria.fr; spf=None smtp.mailfrom=gares AT fettunta.org; spf=None smtp.helo=postmaster AT fettunta.org
Ironport-phdr: 9a23:q1Q3KBdk1FKwswrko0YHohgXlGMj4u6mDksu8pMizoh2WeGdxcu6Yx7h7PlgxGXEQZ/co6odzbGH7ua4ASdbvd6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCzbL52LBi6txndutUZjYZsJas61wfErGZPd+lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLeTQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgzoBOjUk8m/Yl9ZwgbpVrhyhuRJx3o3aYI+aO/ViY6zSf90VSHFdXspNTSFNHp+wYpERA+cHIO1Wr5P9p1wLrRamCgesAvnvyj5UiX/xwKY0zf4uERrd3AwhAtkDt2rbrNPvNKcTTe+1y7PEzSnZYPNNwjf96ZPFchEnofGWXLJ/a9DdyUc1Fw7ciFibtI/rPyuN2+kJvGWX9fRsWOy1h2Mmrwx9uCWjytkuh4XRm44YxFPJ+T99zYs0P9G0VlJ3bcK+HJZQtiyXMZZ9TNk4TGFyoik6z6ULuZ6lcygOz5Qq3xDfZOKbc4iU/xLjUvqRLi1iiHJiYrK/iA6+8UmmyuLiSsm5yFJHoyVfntXSuH0BzR3e58ydRvdg4Eus2y6D1wXJ5eFFJUA0m7DbK5kkwrMomZocq17DETHtmEjtgq+ZaFkk+vS16+ThfrXpvIWQN4huigHxKqgugNCwAfwkMggSWGiW4fiz1Lr6/UHgXLpKiuA2nbLCvZDBJcUbo7a5DBVP3oYi7Ra/FTam384CkXkJNlIWMC6A2oPuIhTFJO3yJfa5mVWl1jlxlN7cObi0L5PXL3PE2IvoZq18oxpRzhAyxtcZ+5tPEbApIfTpW0a3usaOXUxxCBC93+uyUIY17YgZQ2/aWqI=

On Mon, Feb 13, 2017 at 04:40:32PM +0100, Jacques-Henri Jourdan wrote:
> What would happen if you tried to unify your term with an evar that forbids
> this hypothesis?

Coq would not try hard to get rid of the dependency by normalizing the
term. AFAICT Agda does (or used to do) so.

Best,
--
Enrico Tassi

[Coq-Club] efficiently reducing away mentions of a variable, Abhishek Anand, 02/10/2017
- Re: [Coq-Club] efficiently reducing away mentions of a variable, Matthieu Sozeau, 02/13/2017
  - Re: [Coq-Club] efficiently reducing away mentions of a variable, Jacques-Henri Jourdan, 02/13/2017
    - Re: [Coq-Club] efficiently reducing away mentions of a variable, Enrico Tassi, 02/14/2017
- Message not available
  - Message not available
    - Re: [Coq-Club] [coqdev] efficiently reducing away mentions of a variable, Abhishek Anand, 02/14/2017
- Re: [Coq-Club] [coqdev] efficiently reducing away mentions of a variable, Pierre-Marie Pédrot, 02/14/2017