search

HoTT / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
http://coq.inria.fr/
GNU Lesser General Public License v2.1
27 stars 5 forks source link

Change in behavior of [Set Implicit Arguments] #9

Closed JasonGross closed 11 years ago

JasonGross commented 11 years ago

The code

Set Implicit Arguments.

Inductive telescope :=
| Base : forall (A : Type) (B : A -> Type), (forall a, B a) -> (forall a, B a) -> telescope
| Quant : forall A : Type, (A -> telescope) -> telescope.

Fixpoint telescopeOut (t : telescope) :=
  match t with
    | Base _ _ x y => x = y
    | Quant _ f => forall x, telescopeOut (f x)
  end.

fails to compile, informing me that Base expects 3 arguments. Removing Set Implicit Arguments changes this. In 8.4, this succeeds either way.

mattam82 commented 11 years ago

That's due to the new pattern parsing code. Set Asymmetric Patterns will fix it. It's already part of my next patch on HoTT/coq's ssreflect branch which I'll push in a minute.

Le 21 janv. 2013 à 16:24, Jason Gross notifications@github.com a écrit :

The code

Set Implicit Arguments.

Inductive telescope := | Base : forall (A : Type) (B : A -> Type), (forall a, B a) -> (forall a, B a) -> telescope | Quant : forall A : Type, (A -> telescope) -> telescope.

Fixpoint telescopeOut (t : telescope) := match t with | Base x y => x = y | Quant _ f => forall x, telescopeOut (f x) end. fails to compile, informing me that Base expects 3 arguments. Removing Set Implicit Arguments changes this. In 8.4, this succeeds either way.

— Reply to this email directly or view it on GitHub.

-- Matthieu