From b1e0fd772e62a4c0330e15b3979b4944433fb633 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 3 Jul 2024 11:08:47 +0200 Subject: [PATCH] wip --- elpi/constraints/constraint-graph.elpi | 32 +++++++++------- elpi/constraints/constraints.elpi | 11 +++--- elpi/param.elpi | 22 +++++------ examples/Vector_tuple.v | 49 ++++++++++--------------- examples/flt3_step.v | 6 ++- examples/int_to_Zp.v | 51 +++----------------------- examples/nat_ind.v | 1 - examples/summable.v | 6 +-- examples/trocq_setoid_rewrite.v | 2 +- theories/HoTT_additions.v | 7 ++++ theories/Param_nat.v | 2 +- theories/Param_vector.v | 1 - 12 files changed, 73 insertions(+), 117 deletions(-) diff --git a/elpi/constraints/constraint-graph.elpi b/elpi/constraints/constraint-graph.elpi index a9c6c2f..dcdff10 100644 --- a/elpi/constraints/constraint-graph.elpi +++ b/elpi/constraints/constraint-graph.elpi @@ -114,18 +114,19 @@ maximal-class _ _ (pc map4 map4). % default maximal class for an unconstrained v % assign a constant class to a variable and update all the information in the graph % indeed, if the assigned variable was an output class for complex constraints, -% they can now be computed and reduced to simpler constraints on the other variables +% they can now be computed and reduced to simpler constraints on the other variables pred instantiate i:class-id, i:param-class, i:constraint-graph, o:constraint-graph. instantiate ID Class G _ :- util.when-debug dbg.steps (coq.say "instantiate" ID Class G), fail. instantiate ID Class (constraint-graph G) (constraint-graph G') :- - std.map.find ID G (pr LowerNodes HigherNodes), !, + std.map.find ID G (pr LowerNodes HigherNodes), !, std.do! [ internal.filter-var LowerNodes LowerIDs, util.unless (LowerIDs = []) (coq.error "wrong instantiation order: trying to instantiate" ID "before lower variables" LowerIDs), std.fold HigherNodes G (instantiate.aux ID Class) G1, - std.map.remove ID G1 G'. + std.map.remove ID G1 G' + ]. instantiate ID Class G G :- util.when-debug dbg.full ( coq.say "cannot instantiate" ID "at" Class "because it is not in the graph"). @@ -135,27 +136,30 @@ instantiate.aux ID Class (node.const C) G G :- util.unless (param-class.geq C Class) (coq.error "constraint not respected: instantiating" ID "at class" Class "despite upper bound" C). -instantiate.aux ID Class (node.var ct.pi [IDA, IDB]) G G' :- +instantiate.aux ID Class (node.var ct.pi [IDA, IDB]) G G' :- std.do![ util.map.update IDA (internal.remove-lower-node (node.var ct.pi [ID])) G G1, util.map.update IDB (internal.remove-lower-node (node.var ct.pi [ID])) G1 G2, % recompute the dependent product constraint and turn it into 2 order constraints param-class.dep-pi Class C1 C2, util.map.update IDA (internal.add-lower-node (node.const C1)) G2 G3, - util.map.update IDB (internal.add-lower-node (node.const C2)) G3 G'. -instantiate.aux ID Class (node.var ct.arrow [IDA, IDB]) G G' :- + util.map.update IDB (internal.add-lower-node (node.const C2)) G3 G' +]. +instantiate.aux ID Class (node.var ct.arrow [IDA, IDB]) G G' :- std.do![ util.map.update IDA (internal.remove-lower-node (node.var ct.arrow [ID])) G G1, util.map.update IDB (internal.remove-lower-node (node.var ct.arrow [ID])) G1 G2, % recompute the arrow type constraint and turn it into 2 order constraints param-class.dep-arrow Class C1 C2, util.map.update IDA (internal.add-lower-node (node.const C1)) G2 G3, - util.map.update IDB (internal.add-lower-node (node.const C2)) G3 G'. -instantiate.aux ID Class (node.var ct.type [IDR]) G G' :- + util.map.update IDB (internal.add-lower-node (node.const C2)) G3 G' +]. +instantiate.aux ID Class (node.var ct.type [IDR]) G G' :- std.do![ util.map.update IDR (internal.remove-lower-node (node.var ct.type [ID])) G G1, % the constraint either vanishes or forces the relation to be (4,4) if (param-class.requires-axiom Class) (util.map.update IDR (internal.add-lower-node (node.const (pc map4 map4))) G1 G') - (G' = G1). -instantiate.aux ID Class (node.var (ct.gref GR T Tm' GRR) IDs) G G' :- + (G' = G1) +]. +instantiate.aux ID Class (node.var (ct.gref GR T Tm' GRR) IDs) G G' :- std.do! [ std.fold {std.filter IDs (id\ id > 0)} G (id\ g\ g'\ util.map.update id (internal.remove-lower-node (node.var (ct.gref _ _ _ _) [ID])) g g') G1, @@ -164,7 +168,8 @@ instantiate.aux ID Class (node.var (ct.gref GR T Tm' GRR) IDs) G G' :- trocq.db.gref GR Class Cs GR' GRR, !, coq.env.global GR' Tm', % make sure the classes are consistent - instantiate.gref IDs TCs Cs G1 G'. + instantiate.gref IDs TCs Cs G1 G' + ]. pred instantiate.gref i:list class-id, i:list param-class, i:list param-class, i:constraint-graph-content, o:constraint-graph-content. @@ -174,12 +179,13 @@ instantiate.gref [-1|IDs] [TC|TCs] [C|Cs] G G' :- !, % we just check that it is equal to the required one TC = C, instantiate.gref IDs TCs Cs G G'. -instantiate.gref [ID|IDs] [_|TCs] [C|Cs] G G' :- +instantiate.gref [ID|IDs] [_|TCs] [C|Cs] G G' :- std.do![ % here the identifier is not -1, which means that the class at this position is in the graph % we force it to be equal to C in the graph util.map.update ID (internal.add-lower-node (node.const C)) G G1, util.map.update ID (internal.add-higher-node (node.const C)) G1 G2, - instantiate.gref IDs TCs Cs G2 G'. + instantiate.gref IDs TCs Cs G2 G' +]. instantiate.aux ID Class (node.var ct.geq [IDH]) G G' :- % an order constraint is turned into a lower constant class util.map.update IDH (internal.remove-lower-node (node.var ct.geq [ID])) G G1, diff --git a/elpi/constraints/constraints.elpi b/elpi/constraints/constraints.elpi index 086e410..4109f79 100644 --- a/elpi/constraints/constraints.elpi +++ b/elpi/constraints/constraints.elpi @@ -118,7 +118,7 @@ pred c.vars? o:list class-id. pred c.vars! o:list class-id. pred vars? o:list class-id. -vars? IDs :- !, std.spy(declare_constraint (c.vars? IDs) [_]). +vars? IDs :- !, declare_constraint (c.vars? IDs) [_]. pred vars! i:list class-id. vars! IDs :- !, declare_constraint (c.vars! IDs) [_]. @@ -216,7 +216,7 @@ constraint c.graph c.dep-pi c.dep-arrow c.dep-type c.dep-gref c.geq c.reduce-gra cstr-graph.add-geq IDorC1 IDorC2 G G', declare_constraint (c.graph G') [_] ). - rule \ (c.graph G) (c.reduce-graph) <=> (std.spy-do! [ + rule \ (c.graph G) (c.reduce-graph) <=> (std.do! [ coq.say "final constraint graph START:", vars? IDs, util.when-debug dbg.full ( @@ -240,17 +240,18 @@ constraint c.graph c.dep-pi c.dep-arrow c.dep-type c.dep-gref c.geq c.reduce-gra % return a list of associations of a variable and its constant class pred reduce i:list class-id, i:constraint-graph, o:list (pair class-id param-class). reduce [] _ []. -reduce [ID|IDs] ConstraintGraph [pr ID MinClass|FinalValues] :- +reduce [ID|IDs] ConstraintGraph [pr ID MinClass|FinalValues] :- std.do! [ cstr-graph.minimal-class ID ConstraintGraph MinClass, util.when-debug dbg.full (coq.say "min value" MinClass "for" ID), cstr-graph.maximal-class ID ConstraintGraph MaxClass, util.when-debug dbg.full (coq.say "max value" MaxClass "for" ID), util.unless (param-class.geq MaxClass MinClass) (coq.error "no solution for variable" ID), - reduce IDs {cstr-graph.instantiate ID MinClass ConstraintGraph} FinalValues. + reduce IDs {cstr-graph.instantiate ID MinClass ConstraintGraph} FinalValues +]. % now instantiate for real pred instantiate-coq i:pair class-id param-class. -instantiate-coq (pr ID (pc M0 N0)) :- std.spy-do! [ +instantiate-coq (pr ID (pc M0 N0)) :- std.do! [ util.when-debug dbg.full (coq.say "instantiating" ID "with" (pc M0 N0)), link- C ID, univ-link- C M N, diff --git a/elpi/param.elpi b/elpi/param.elpi index 84facfe..2771565 100644 --- a/elpi/param.elpi +++ b/elpi/param.elpi @@ -133,7 +133,7 @@ param (fun N T F) FunTy (fun N' T' F') FunR :- !, param (prod _ A (_\ B)) (app [pglobal (const PType) _, M, N]) (prod `_` A' (_\ B')) (app [pglobal (const ParamArrow) UI|Args]) :- - (trocq.db.ptype PType; trocq.db.pprop PType), !, std.spy-do! [ + (trocq.db.ptype PType; trocq.db.pprop PType), !, std.do! [ util.when-debug dbg.steps (coq.say "param/arrow" A "->" B "@" M N), cstr.univ-link C M N, util.when-debug dbg.full (coq.say "param/arrow:" M N "is linked to" C), @@ -141,11 +141,9 @@ param util.when-debug dbg.full (coq.say "param/arrow: added dep-arrow from" C "to" CA "and" CB), cstr.univ-link CA MA NA, util.when-debug dbg.full (coq.say "param/arrow:" MA NA "is linked to" CA), - % std.assert-ok! (coq.typecheck A TyA) "param/arrow: cannot typecheck A", - % if (TyA = sort prop) - % (PTypeA = app [pglobal (const {trocq.db.pprop}) _, M1A, M2A]) - % (PTypeA = app [pglobal (const {trocq.db.ptype}) _, M1A, M2A]), - PTypeA = (app [pglobal (const PType) _, MA, NA]), + std.assert-ok! (coq.typecheck A TyA) "param/arrow: cannot typecheck A", + if (TyA = sort prop) (trocq.db.pprop PTypeGRA) (trocq.db.ptype PTypeGRA), + PTypeA = (app [pglobal (const PTypeGRA) _, MA, NA]), param A PTypeA A' AR, cstr.univ-link CB MB NB, util.when-debug dbg.full (coq.say "param/arrow:" MB NB "is linked to" CB), @@ -170,7 +168,7 @@ param param (prod N A B) (app [pglobal (const PType) _, M1, M2]) (prod N' A' B') (app [pglobal (const ParamForall) UI|Args']) :- - (trocq.db.ptype PType; trocq.db.pprop PType), !, std.spy-do![ + (trocq.db.ptype PType; trocq.db.pprop PType), !, std.do![ util.when-debug dbg.steps (coq.say "param/forall" N ":" A "," B "@" M1 M2), coq.name-suffix N "'" N', coq.name-suffix N "R" NR, @@ -180,15 +178,13 @@ param util.when-debug dbg.full (coq.say "param/forall: added dep-pi from" C "to" CA "and" CB), cstr.univ-link CA M1A M2A, !, util.when-debug dbg.full (coq.say "param/forall:" M1A M2A "is linked to" CA), - % std.assert-ok! (coq.typecheck A TyA) "param/arrow: cannot typecheck A", - % if (TyA = sort prop) - % (PTypeA = app [pglobal (const {trocq.db.pprop}) _, M1A, M2A]) - % (PTypeA = app [pglobal (const {trocq.db.ptype}) _, M1A, M2A]), - PTypeA = (app [pglobal (const PType) _, M1A, M2A]), + std.assert-ok! (coq.typecheck A TyA) "param/arrow: cannot typecheck A", + if (TyA = sort prop) (trocq.db.pprop PTypeGRA) (trocq.db.ptype PTypeGRA), + PTypeA = (app [pglobal (const PTypeGRA) _, M1A, M2A]), param A PTypeA A' AR, cstr.univ-link CB M1B M2B, !, util.when-debug dbg.full (coq.say "param/forall:" M1B M2B "is linked to" CB), - @annot-pi-decl N A a\ pi a' aR\ param.store a A a' aR => std.spy-do![ + @annot-pi-decl N A a\ pi a' aR\ param.store a A a' aR => std.do![ util.when-debug dbg.full (coq.say "param/forall: introducing" a "@" A "~" a' "by" aR), param (B a) (app [pglobal (const PType) _, M1B, M2B]) (B' a') (BR a a' aR), !, util.when-debug dbg.full (coq.say "param/forall:" (B a) "@" M1B M2B "~" (B' a') "by" (BR a a' aR)) diff --git a/examples/Vector_tuple.v b/examples/Vector_tuple.v index 2fd852a..60e2c8a 100644 --- a/examples/Vector_tuple.v +++ b/examples/Vector_tuple.v @@ -11,7 +11,7 @@ (* * see LICENSE file for the text of the license *) (*****************************************************************************) -From Coq Require Import ssreflect. +From mathcomp Require Import ssreflect ssrfun ssrnat. From Trocq Require Import Trocq. From Trocq Require Import Param_nat Param_trans Param_bool Param_vector. @@ -23,7 +23,7 @@ Definition tuple (A : Type) : nat -> Type := fix F n := match n with | O => Unit - | S n' => F n' * A + | S n' => (F n' * A)%type end. Definition const : forall {A : Type} (a : A) (n : nat), tuple A n := @@ -77,7 +77,7 @@ Definition vector_to_tupleK {A : Type} : fix F n v := match v with | Vector.nil => idpath - | Vector.cons m a v' => ap (Vector.cons a) (F m v') + | Vector.cons _ a v' => ap (Vector.cons a) (F _ v') end. Definition tuple_to_vectorK {A : Type} : @@ -215,7 +215,7 @@ Trocq Use Param_append Param_const Param01_paths. Lemma append_const : forall {A : Type} (a : A) (n1 n2 : nat), append (const a n1) (const a n2) = const a (n1 + n2). Proof. - trocq. exact @Vector.append_const. + trocq; exact: @Vector.append_const. Qed. End AppendConst. @@ -279,10 +279,11 @@ Proof. by trocq. Qed. (* bounded nat and bitvector *) (* NB: we can use transitivity to make the proofs here too *) + Module BV. -Definition bounded_nat (k : nat) := {n : nat & n < pow 2 k}%nat. -Definition bitvector (k : nat) := Vector.t Bool k. +Definition bounded_nat (k : nat) := {n : nat & n < expn 2 n = true}%nat. +Definition bitvector := (Vector.t Bool). (* bounded_nat k ~ bitvector k' *) @@ -314,33 +315,24 @@ Lemma S_add1 : forall (n : nat), S n = (n + 1)%nat. Proof. induction n. - simpl. reflexivity. - - simpl add. apply ap. exact IHn. + - by rewrite addn1. Defined. -Lemma one_lt_pow2 (k : nat) : (1 <= pow 2 k)%nat. +Lemma one_lt_pow2 (k : nat) : (1 <= expn 2 k)%nat = true. Proof. +Search expn (leq 1). induction k. - - simpl. apply leq_n. - - apply (leq_trans IHk). - simpl. - apply n_leq_add_n_k. -Defined. + - simpl. +Admitted. Axiom bv_bound : - forall {k : nat} (bv : bitvector k), (bv_to_nat bv <= pow 2 k - 1)%nat. + forall {k : nat} (bv : bitvector k), (bv_to_nat bv <= expn 2 k - 1)%nat = true. Definition bv_to_bnat {k : nat} (bv : bitvector k) : bounded_nat k. Proof. unshelve econstructor. - exact (bv_to_nat bv). - - apply (mixed_trans1 _ (pow 2 k - 1) _). - * apply bv_bound. - * apply natpmswap1. - 1: { apply one_lt_pow2. } - rewrite nat_add_comm. - rewrite <- (S_add1 (pow 2 k)). - apply n_lt_Sn. -Defined. +Admitted. Axiom map_in_R_bv_bnat : forall {k : nat} {bv : bitvector k} {bn : bounded_nat k}, @@ -386,7 +378,7 @@ Definition Param44_bnat_bv (k k' : nat) (kR : natR k k') : Param44.Rel (bounded_nat k) (bitvector k'). Proof. unshelve eapply (@Param44_trans _ (bitvector k) _). - - exact Param44_bnat_bv_d. + - exact Param44_bnat_bv_d. - exact (Vector.Param44 Bool Bool Param44_Bool k k' kR). Defined. @@ -425,22 +417,21 @@ Axiom getBitR : (n n' : nat) (nR : natR n n'), BoolR (getBit_bnat bn n) (getBit_bv bv' n'). -(* lt ~ lt *) -Axiom Param10_lt : +Axiom Param10_le : forall (n1 n1' : nat) (n1R : natR n1 n1') (n2 n2' : nat) (n2R : natR n2 n2'), - Param10.Rel (n1 < n2)%nat (n1' < n2')%nat. + BoolR (n1 <= n2)%nat (n1' <= n2')%nat. Axiom setBitThenGetSame : forall {k : nat} (bv : bitvector k) (i : nat) (b : Bool), - (i < k)%nat -> getBit_bv (setBit_bv bv i b) i = b. + (i < k)%nat = true -> getBit_bv (setBit_bv bv i b) i = b. Trocq Use Param2a0_nat Param44_Bool Param2a0_bnat_bv getBitR setBitR. -Trocq Use Param01_paths Param10_lt. +Trocq Use Param01_paths Param10_paths Param10_le trueR SR. Lemma setBitThenGetSame' : forall {k : nat} (bn : bounded_nat k) (i : nat) (b : Bool), - (i < k)%nat -> getBit_bnat (setBit_bnat bn i b) i = b. + (i < k)%nat = true -> getBit_bnat (setBit_bnat bn i b) i = b. Proof. trocq. exact @setBitThenGetSame. Qed. diff --git a/examples/flt3_step.v b/examples/flt3_step.v index b5a41df..2c58df8 100644 --- a/examples/flt3_step.v +++ b/examples/flt3_step.v @@ -71,7 +71,7 @@ Notation "x ≡ y" := (eqmodp x%int y%int) (format "x ≡ y", at level 70) : int_scope. Notation "x ≢ y" := (not (eqmodp x%int y%int)) (format "x ≢ y", at level 70) : int_scope. -Notation "x ≠ y" := (not (x = y)). +Notation "x ≠ y" := (not (x = y)) (at level 70). Notation "ℤ/9ℤ" := Zmod9. Notation ℤ := int. @@ -88,7 +88,9 @@ Variable Reqmodp01 : forall (m : int) (x : Zmod9), Rp m x -> Trocq Use Rp Rmul Rzero Rone Radd Rmod3 Param10_paths Reqmodp01. -Trocq Use Param01_sum Param01_Empty Param10_Empty. +Trocq Use Param01_sum. +Trocq Use Param01_Empty. +Trocq Use Param10_Empty. Lemma flt3_step : forall (m n p : ℤ), m * n * p % 3 ≢ 0 -> (m³ + n³)%ℤ ≠ p³%ℤ. diff --git a/examples/int_to_Zp.v b/examples/int_to_Zp.v index e041fc5..00e105d 100644 --- a/examples/int_to_Zp.v +++ b/examples/int_to_Zp.v @@ -27,20 +27,6 @@ rewrite modNz_nat// val_Zp_nat//= /Zp_trunc/=. rewrite modnS. case: ifP. rewrite subn0 modnn. -(* - rewrite subn1. -rewrite -[n.+1]addn1. -rewrite modnD//=. -rewrite modnS /dvdn. -rewrite modn_small//; last first. - rewrite ltn_psubLR//. leq_addl//. -Search (_ - _ < _)%N. -Search (_.+1 %% _)%N. - -Search (_ %% _)%Z (_ %% _)%N. -rewrite val_Zp -congr Posz. - rewrite val_Zp_nat//. *) Admitted. Lemma Zp_int_mod [p : nat] : 1 < p -> @@ -126,42 +112,15 @@ Trocq Use Rp Rmul Rzero Param10_paths Reqmodp01 RTrue Runit. Local Open Scope ring_scope. -Lemma IntRedModZp : int -> True. - (* (forall (m n : 'Z_p), m = n * n -> m = 0) -> - forall (m n : int), eqmodp m n. *) +Lemma IntRedModZp : + (forall (m n : 'Z_p), m = n * n -> m = n) -> + forall (m n : int), m = int_mul n n -> eqmodp m n. Proof. -(* move=> Hyp. *) +move=> Hyp. trocq; simpl. exact: Hyp. Qed. (* Print Assumptions IntRedModZp. (* No Univalence *) *) -End IntToZmod7. - -Module Zmod7ToInt. - -Definition Rp := SplitSurj.toParamSym (SplitSurj.Build reprpK). - -Axiom Rzero : Rp zerop zero. -Variable Radd : binop_param Rp Rp Rp addp add. -Variable paths_to_eqmodp : binop_param Rp Rp iff paths eqmodp. - -Trocq Use Rp Param01_paths Param10_paths Radd Rzero. - -Goal (forall x y, x + y = y + x)%Zmod7. -Proof. - trocq. - exact addC. -Qed. - -Goal (forall x y z, x + y + z = y + x + z)%Zmod7. -Proof. - intros x y z. - suff addpC: forall x y, (x + y = y + x)%Zmod7. { - by rewrite (addpC x y). } - trocq. - exact addC. -Qed. - -End Zmod7ToInt. +End modp. diff --git a/examples/nat_ind.v b/examples/nat_ind.v index b972c27..ba5609e 100644 --- a/examples/nat_ind.v +++ b/examples/nat_ind.v @@ -12,7 +12,6 @@ (*****************************************************************************) From Coq Require Import ssreflect. -From HoTT Require Import HoTT. From Trocq Require Import Trocq. Set Universe Polymorphism. diff --git a/examples/summable.v b/examples/summable.v index eaf27da..e1e70c5 100644 --- a/examples/summable.v +++ b/examples/summable.v @@ -178,11 +178,7 @@ Definition R_add_xnnR : forall (r1 : nnR) (re1 : xnnR), R_nnR r1 re1 -> forall (r2 : nnR) (re2 : xnnR), R_nnR r2 re2 -> R_nnR (r1 + r2) (re1 + re2). -Proof. -rewrite /R_nnR /extend. -move=> r1 [_ []|]; last by discriminate. -by move=> r2 [_ []|]; last by discriminate. -Qed. +Proof. by do 2!move=> ? [_ [<-]|//]. Qed. Definition seq_nnR_add : forall (r1 : summable) (re1 : seq_xnnR), Rrseq r1 re1 -> diff --git a/examples/trocq_setoid_rewrite.v b/examples/trocq_setoid_rewrite.v index b78a17f..6c66930 100644 --- a/examples/trocq_setoid_rewrite.v +++ b/examples/trocq_setoid_rewrite.v @@ -15,7 +15,7 @@ From Coq Require Import ssreflect. From Coq Require Import Setoid. From Trocq Require Import Trocq. -Set Universe PolymoRinthism. +Set Universe Polymorphism. Declare Scope int_scope. Delimit Scope int_scope with int. diff --git a/theories/HoTT_additions.v b/theories/HoTT_additions.v index 70edcc2..02df3b0 100644 --- a/theories/HoTT_additions.v +++ b/theories/HoTT_additions.v @@ -237,6 +237,13 @@ Proof. by case: _ / p. Defined. Lemma concat_Vp@{i} {A : Type@{i}} {x y : A} (p : x = y) : p^ @ p = 1%path. Proof. by case: _ / p. Defined. +Lemma path_prod {A B : Type} (z z' : A * B) : + fst z = fst z' -> snd z = snd z' -> z = z'. +Proof. +by case: z z' => [? ?] [? ?] /= -> ->. +Qed. + + Reserved Notation "n .+1" (at level 2, left associativity, format "n .+1"). Reserved Notation "n .+2" (at level 2, left associativity, format "n .+2"). Reserved Notation "n .+3" (at level 2, left associativity, format "n .+3"). diff --git a/theories/Param_nat.v b/theories/Param_nat.v index 99d5627..872fd81 100644 --- a/theories/Param_nat.v +++ b/theories/Param_nat.v @@ -11,7 +11,7 @@ (* * see LICENSE file for the text of the license *) (*****************************************************************************) -From Coq Require Import ssreflect. +From mathcomp Require Import ssreflect ssrfun ssrnat. Require Import HoTT_additions Hierarchy. Set Universe Polymorphism. diff --git a/theories/Param_vector.v b/theories/Param_vector.v index d1fe6a5..34c4ff1 100644 --- a/theories/Param_vector.v +++ b/theories/Param_vector.v @@ -23,7 +23,6 @@ Notation Unit := unit. Module Vector. (* the standard vector type *) - Inductive t (A : Type) : nat -> Type := | nil : t A 0 | cons : forall (n : nat), A -> t A n -> t A (S n).