Skip to content
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

fix mode signature #736

Merged
merged 1 commit into from
Dec 16, 2024
Merged

fix mode signature #736

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 apps/derive/elpi/eqb.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
/* license: GNU Lesser General Public License Version 2.1 or later */
/* ------------------------------------------------------------------------- */

type feqb.trm->term trm -> term -> prop.
pred feqb.trm->term i:trm, o:term.

macro @pi-trm N T F :-
pi x xx\ decl x N T => (feqb.trm->term xx x :- !) => F xx x.
Expand Down
2 changes: 1 addition & 1 deletion apps/derive/elpi/eqbOK.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
/* ------------------------------------------------------------------------- */


type feqb.trm->term trm -> term -> prop.
pred feqb.trm->term i:trm, o:term.

macro @pi-trm N T F :-
pi x xx\ decl x N T => (feqb.trm->term xx x :- !) => F xx x.
Expand Down
2 changes: 1 addition & 1 deletion apps/derive/elpi/eqbcorrect.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
/* license: GNU Lesser General Public License Version 2.1 or later */
/* ------------------------------------------------------------------------- */

type feqb.trm->term trm -> term -> prop.
pred feqb.trm->term i:trm, o:term.

macro @pi-trm N T F :-
pi x xx\ decl x N T => (feqb.trm->term xx x :- !) => F xx x.
Expand Down
2 changes: 1 addition & 1 deletion apps/derive/theories/derive/eq.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ type eq-for inductive -> constant -> prop.
#[superglobal] Elpi Accumulate derive.eq.db File derive.lib.
#[superglobal] Elpi Accumulate derive.eq.db lp:{{

type whd1 term -> term -> prop.
pred whd1 i:term, o:term.

:name "eq-db:fail"
eq-db A B F :-
Expand Down
2 changes: 1 addition & 1 deletion apps/derive/theories/derive/eqb.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ Require Import eqType_ast tag fields.
Register eqb_body as elpi.derive.eqb_body.

Elpi Db derive.eqb.db lp:{{
type whd1 term -> term -> prop.
pred whd1 i:term, o:term.

pred eqb-done o:gref.

Expand Down
2 changes: 1 addition & 1 deletion apps/tc/elpi/ho_link.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -130,7 +130,7 @@ namespace tc {
}
}

pred eta i:term, o:term.
pred eta i:term, i:term.
eta A B :- eta.eta A B.

pred solve-eta.
Expand Down
9 changes: 0 additions & 9 deletions apps/tc/theories/add_commands.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,23 +18,14 @@ Set Warnings "+elpi".

Elpi Command TC.AddAllInstances.
Elpi Accumulate Db tc.db.

Elpi Accumulate Db tc_options.db.

Elpi Accumulate File tc_aux.

Elpi Accumulate File ho_precompile.

Elpi Accumulate File unif.

Elpi Accumulate File ho_link.

Elpi Accumulate File ho_compile.

Elpi Accumulate File compiler1.

Elpi Accumulate File modes.

Elpi Accumulate lp:{{
main L :-
args->str-list L L1,
Expand Down
3 changes: 3 additions & 0 deletions apps/tc/theories/db.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -99,6 +99,9 @@ Elpi Db tc.db lp:{{
pred dummy.

pred ho-link o:term, i:term, o:A.
pred link.eta i:term, i:term.
pred link.llam i:term, i:term.

}
}}.
From elpi.apps.tc.elpi Extra Dependency "base.elpi" as base.
Expand Down
Loading