Skip to content

remove typechecking warnings #466

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Nov 28, 2024
Merged

remove typechecking warnings #466

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion tests/unit/close_hole_term.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ From elpi Require Import elpi.
From Coq Require Export Setoid.

Elpi Query HB.instance lp:{{
X = app [{{list}}, Y],
X = app [{{list}}, Y_],
% X needs to be typechecked here to get rid of the hole for the type of Y
coq.typecheck X _ ok,
abstract-holes.main X Z,
Expand Down
6 changes: 3 additions & 3 deletions tests/unit/enrich_type.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,19 +9,19 @@ Elpi Query HB.structure lp:{{

Elpi Query HB.structure lp:{{
saturate-type-constructor {{list}} X,
std.assert! (X = app [{{list}}, Y]) "wrong enriched type"
std.assert! (X = app [{{list}}, Y_]) "wrong enriched type"
}}.

Elpi Query HB.structure lp:{{
Y = (x \ (y \ {{(prod (list lp:x) (list lp:y))}})),
saturate-type-constructor (Y _ _) X,
std.assert! (X = (app [{{prod}}, (app[{{list}},X1]), app[{{list}},C]])) "wrong enriched type"
std.assert! (X = (app [{{prod}}, (app[{{list}},X1_]), app[{{list}},C_]])) "wrong enriched type"
}}.

Class Inj {A B} (R : relation A) (S : relation B) (f : A -> B) : Prop :=
inj x y : S (f x) (f y) -> R x y.

Elpi Query HB.structure lp:{{
saturate-type-constructor {{Inj}} X,
std.assert! (X = app [(global (const Inj)), A, B, R, S, F]) "wrong enriched type"
std.assert! (X = app [(global (const Inj_)), A_, B_, R_, S_, F_]) "wrong enriched type"
}}.
4 changes: 2 additions & 2 deletions tests/unit/mixin_src_has_mixin_instance.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ HB.instance Definition nat_m2 : m2 nat := m2.Build nat 1.


Elpi Query HB.instance lp:{{
mixin-src->has-mixin-instance (mixin-src {{nat}} M1 {{nat_m1}}) Y,
mixin-src->has-mixin-instance (mixin-src {{nat}} M1_ {{nat_m1}}) Y,
Y = has-mixin-instance (cs-gref {{:gref nat}}) {{:gref m1.phant_axioms}} {{:gref nat_m1}}.

}}.
Expand All @@ -22,7 +22,7 @@ Section Test.
Variable X:s1.type.

Elpi Query HB.instance lp:{{
mixin-src->has-mixin-instance (mixin-src {{list X}} M1 {{i1 X}}) Y,
mixin-src->has-mixin-instance (mixin-src {{list X}} M1_ {{i1 X}}) Y,
Y = has-mixin-instance (cs-gref {{:gref list}}) {{:gref m1.phant_axioms}} {{:gref i1}}.

}}.
Expand Down
2 changes: 1 addition & 1 deletion tests/unit/struct.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ HB.structure Definition foo1 := { A of is_foo (option nat) A & m1 A}.


Elpi Query HB.structure lp:{{
std.findall (has-mixin-instance _ _ _) H
std.findall (has-mixin-instance _ _ _) H_
}}.

(* here we don't have any declared instances but a clause is still created by the system :
Expand Down
Loading