Skip to content

Commit

Permalink
Avoid mentioning auto-generated names
Browse files Browse the repository at this point in the history
  • Loading branch information
@pi8027
pi8027 committed Sep 22, 2023
1 parent 04581af commit 1bb41b4
Show file tree
Hide file tree
Showing 6 changed files with 148 additions and 73 deletions.
107 changes: 81 additions & 26 deletions theories/common.elpi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -82,6 +82,52 @@ pred negb i:bool, o:bool.
negb tt ff :- !.
negb ff tt :- !.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

pred register-instance i:scope, i:id, i:gref, i:gref, i:constant -> prop.
register-instance Scope DbName Proj Pat Pred :- std.do! [
coq.CS.db-for Proj (cs-gref Pat) [cs-instance _ _ (const Inst)],
coq.elpi.accumulate Scope DbName (clause _ _ (Pred Inst :- !)) ].

pred canonical-init i:scope, i:id.
canonical-init Scope DbName :- std.do! [
register-instance Scope DbName
{{:gref GRing.Nmodule.sort }} {{:gref nat }} canonical-nat-nmodule,
register-instance Scope DbName
{{:gref GRing.SemiRing.sort }} {{:gref nat }} canonical-nat-semiring,
register-instance Scope DbName
{{:gref GRing.ComSemiRing.sort }} {{:gref nat }} canonical-nat-comsemiring,
register-instance Scope DbName
{{:gref GRing.Nmodule.sort }} {{:gref N }} canonical-N-nmodule,
register-instance Scope DbName
{{:gref GRing.SemiRing.sort }} {{:gref N }} canonical-N-semiring,
register-instance Scope DbName
{{:gref GRing.ComSemiRing.sort }} {{:gref N }} canonical-N-comsemiring,
register-instance Scope DbName
{{:gref GRing.Nmodule.sort }} {{:gref int }} canonical-int-nmodule,
register-instance Scope DbName
{{:gref GRing.Zmodule.sort }} {{:gref int }} canonical-int-zmodule,
register-instance Scope DbName
{{:gref GRing.SemiRing.sort }} {{:gref int }} canonical-int-semiring,
register-instance Scope DbName
{{:gref GRing.Ring.sort }} {{:gref int }} canonical-int-ring,
register-instance Scope DbName
{{:gref GRing.ComRing.sort }} {{:gref int }} canonical-int-comring,
register-instance Scope DbName
{{:gref GRing.UnitRing.sort }} {{:gref int }} canonical-int-unitring,
register-instance Scope DbName
{{:gref GRing.Nmodule.sort }} {{:gref Z }} canonical-Z-nmodule,
register-instance Scope DbName
{{:gref GRing.Zmodule.sort }} {{:gref Z }} canonical-Z-zmodule,
register-instance Scope DbName
{{:gref GRing.SemiRing.sort }} {{:gref Z }} canonical-Z-semiring,
register-instance Scope DbName
{{:gref GRing.Ring.sort }} {{:gref Z }} canonical-Z-ring,
register-instance Scope DbName
{{:gref GRing.ComRing.sort }} {{:gref Z }} canonical-Z-comring,
register-instance Scope DbName
{{:gref GRing.UnitRing.sort }} {{:gref Z }} canonical-Z-unitring ].

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Expression refifier

Expand Down Expand Up @@ -134,32 +180,35 @@ type rmorphism-Z rmorphism. % (int_of_Z _)%:~R

pred rmorphism->nmod i:rmorphism, o:term.
rmorphism->nmod (rmorphism U _ _ _ _ _ _) U :- !.
rmorphism->nmod rmorphism-nat {{ nat_nmodType }} :- !.
rmorphism->nmod rmorphism-N {{ N_nmodType }} :- !.
rmorphism->nmod rmorphism-int {{ int_nmodType }} :- !.
rmorphism->nmod rmorphism-Z {{ Z_nmodType }} :- !.
rmorphism->nmod rmorphism-nat (global (const U)) :- !, canonical-nat-nmodule U.
rmorphism->nmod rmorphism-N (global (const U)) :- !, canonical-N-nmodule U.
rmorphism->nmod rmorphism-int (global (const U)) :- !, canonical-int-nmodule U.
rmorphism->nmod rmorphism-Z (global (const U)) :- !, canonical-Z-nmodule U.

pred rmorphism->zmod i:rmorphism, o:term.
rmorphism->zmod (rmorphism _ (some U) _ _ _ _ _) U :- !.
rmorphism->zmod rmorphism-int {{ int_zmodType }} :- !.
rmorphism->zmod rmorphism-Z {{ Z_zmodType }} :- !.
rmorphism->zmod rmorphism-int (global (const U)) :- !, canonical-int-zmodule U.
rmorphism->zmod rmorphism-Z (global (const U)) :- !, canonical-Z-zmodule U.

pred rmorphism->sring i:rmorphism, o:term.
rmorphism->sring (rmorphism _ _ R _ _ _ _) R :- !.
rmorphism->sring rmorphism-nat {{ nat_semiRingType }} :- !.
rmorphism->sring rmorphism-N {{ N_semiRingType }} :- !.
rmorphism->sring rmorphism-int {{ int_semiRingType }} :- !.
rmorphism->sring rmorphism-Z {{ Z_semiRingType }} :- !.
rmorphism->sring rmorphism-nat (global (const R)) :- !,
canonical-nat-semiring R.
rmorphism->sring rmorphism-N (global (const R)) :- !, canonical-N-semiring R.
rmorphism->sring rmorphism-int (global (const R)) :- !,
canonical-int-semiring R.
rmorphism->sring rmorphism-Z (global (const R)) :- !, canonical-Z-semiring R.

pred rmorphism->ring i:rmorphism, o:term.
rmorphism->ring (rmorphism _ _ _ (some R) _ _ _) R :- !.
rmorphism->ring rmorphism-int {{ int_ringType }} :- !.
rmorphism->ring rmorphism-Z {{ Z_ringType }} :- !.
rmorphism->ring rmorphism-int (global (const R)) :- !, canonical-int-ring R.
rmorphism->ring rmorphism-Z (global (const R)) :- !, canonical-Z-ring R.

pred rmorphism->uring i:rmorphism, o:term.
rmorphism->uring (rmorphism _ _ _ _ (some UR) _ _) UR :- !.
rmorphism->uring rmorphism-int {{ int_unitRingType }} :- !.
rmorphism->uring rmorphism-Z {{ Z_unitRingType }} :- !.
rmorphism->uring rmorphism-int (global (const R)) :- !,
canonical-int-unitring R.
rmorphism->uring rmorphism-Z (global (const R)) :- !, canonical-Z-unitring R.

pred rmorphism->field i:rmorphism, o:term.
rmorphism->field (rmorphism _ _ _ _ _ (some F) _) F :- !.
Expand Down Expand Up @@ -297,25 +346,27 @@ pred nmod.additive i:term, i:additive, i:term -> term, i:term, i:term,
o:term, o:term, o:list term.
nmod.additive V (additive U _ Morph) NewMorph NewMorphInst In1
{{ @MnatAdditive lp:U lp:NewMorphInst lp:OutM1 }} Out VM :-
coq.unify-eq V {{ nat_nmodType }} ok,
coq.unify-eq V (global (const { canonical-nat-nmodule })) ok,
mem VM (Morph (NewMorph {{ 1%N }})) N, !,
ring rmorphism-nat In1 OutM1 Out1 VM, !,
build.mul { build.variable { positive-constant {calc (N + 1)} } } Out1 Out.
nmod.additive V (additive U _ Morph) NewMorph NewMorphInst In1
{{ @MNAdditive lp:U lp:NewMorphInst lp:OutM1 }} Out VM :-
coq.unify-eq V {{ N_nmodType }} ok,
coq.unify-eq V (global (const { canonical-N-nmodule })) ok,
mem VM (Morph (NewMorph {{ 1%num }})) N, !,
ring rmorphism-N In1 OutM1 Out1 VM, !,
build.mul { build.variable { positive-constant {calc (N + 1)} } } Out1 Out.
nmod.additive V (additive U _ Morph) NewMorph NewMorphInst In1
{{ @MintAdditive lp:U lp:NewMorphInst lp:OutM1 }} Out VM :-
target-zmodule _, coq.unify-eq V {{ int_nmodType }} ok,
target-zmodule _,
coq.unify-eq V (global (const { canonical-int-nmodule })) ok,
mem VM (Morph (NewMorph {{ 1%Z }})) N, !,
ring rmorphism-int In1 OutM1 Out1 VM, !,
build.mul { build.variable { positive-constant {calc (N + 1)} } } Out1 Out.
nmod.additive V (additive U _ Morph) NewMorph NewMorphInst In1
{{ @MZAdditive lp:U lp:NewMorphInst lp:OutM1 }} Out VM :-
target-zmodule _, coq.unify-eq V {{ Z_nmodType }} ok,
target-zmodule _,
coq.unify-eq V (global (const { canonical-Z-nmodule })) ok,
mem VM (Morph (NewMorph {{ Zpos 1 }})) N, !,
ring rmorphism-Z In1 OutM1 Out1 VM, !,
build.mul { build.variable { positive-constant {calc (N + 1)} } } Out1 Out.
Expand Down Expand Up @@ -557,22 +608,24 @@ pred ring.rmorphism i:term, i:rmorphism, i:term -> term, i:term, i:term,
o:term, o:term, o:list term.
ring.rmorphism S C _ NewMorphInst In1
{{ @RnatMorph lp:R lp:NewMorphInst lp:OutM1 }} Out1 VM :-
coq.unify-eq S {{ nat_semiRingType }} ok, !,
coq.unify-eq S (global (const { canonical-nat-semiring })) ok, !,
rmorphism->sring C R, !,
ring rmorphism-nat In1 OutM1 Out1 VM.
ring.rmorphism S C _ NewMorphInst In1
{{ @RNMorph lp:R lp:NewMorphInst lp:OutM1 }} Out1 VM :-
coq.unify-eq S {{ N_semiRingType }} ok, !,
coq.unify-eq S (global (const { canonical-N-semiring })) ok, !,
rmorphism->sring C R, !,
ring rmorphism-N In1 OutM1 Out1 VM.
ring.rmorphism S C _ NewMorphInst In1
{{ @RintMorph lp:R lp:NewMorphInst lp:OutM1 }} Out1 VM :-
target-zmodule _, coq.unify-eq S {{ int_semiRingType }} ok, !,
target-zmodule _,
coq.unify-eq S (global (const { canonical-int-semiring })) ok, !,
rmorphism->sring C R, !,
ring rmorphism-int In1 OutM1 Out1 VM.
ring.rmorphism S C _ NewMorphInst In1
{{ @RZMorph lp:R lp:NewMorphInst lp:OutM1 }} Out1 VM :-
target-zmodule _, coq.unify-eq S {{ Z_semiRingType }} ok, !,
target-zmodule _,
coq.unify-eq S (global (const { canonical-Z-semiring })) ok, !,
rmorphism->sring C R, !,
ring rmorphism-Z In1 OutM1 Out1 VM.
ring.rmorphism S C NewMorph NewMorphInst In1
Expand All @@ -586,28 +639,30 @@ pred ring.additive i:term, i:rmorphism, i:term -> term, i:term, i:term,
o:term, o:term, o:list term.
ring.additive V C NewMorph NewMorphInst In1
{{ @RnatAdditive lp:R lp:NewMorphInst lp:OutM1 }} Out VM :-
coq.unify-eq V {{ nat_nmodType }} ok,
coq.unify-eq V (global (const { canonical-nat-nmodule })) ok,
rmorphism->sring C R, rmorphism->morph C Morph,
mem VM (Morph (NewMorph {{ 1%N }})) N, !,
ring rmorphism-nat In1 OutM1 Out1 VM, !,
build.mul { build.variable { positive-constant {calc (N + 1)} } } Out1 Out.
ring.additive V C NewMorph NewMorphInst In1
{{ @RNAdditive lp:R lp:NewMorphInst lp:OutM1 }} Out VM :-
coq.unify-eq V {{ N_nmodType }} ok,
coq.unify-eq V (global (const { canonical-N-nmodule })) ok,
rmorphism->sring C R, rmorphism->morph C Morph,
mem VM (Morph (NewMorph {{ 1%num }})) N, !,
ring rmorphism-N In1 OutM1 Out1 VM, !,
build.mul { build.variable { positive-constant {calc (N + 1)} } } Out1 Out.
ring.additive V C NewMorph NewMorphInst In1
{{ @RintAdditive lp:R lp:NewMorphInst lp:OutM1 }} Out VM :-
target-zmodule _, coq.unify-eq V {{ int_nmodType }} ok,
target-zmodule _,
coq.unify-eq V (global (const { canonical-int-nmodule })) ok,
rmorphism->sring C R, rmorphism->morph C Morph,
mem VM (Morph (NewMorph {{ 1%Z }})) N, !,
ring rmorphism-int In1 OutM1 Out1 VM, !,
build.mul { build.variable { positive-constant {calc (N + 1)} } } Out1 Out.
ring.additive V C NewMorph NewMorphInst In1
{{ @RZAdditive lp:R lp:NewMorphInst lp:OutM1 }} Out VM :-
target-zmodule _, coq.unify-eq V {{ Z_nmodType }} ok,
target-zmodule _,
coq.unify-eq V (global (const { canonical-Z-nmodule })) ok,
rmorphism->sring C R, rmorphism->morph C Morph,
mem VM (Morph (NewMorph {{ Zpos 1 }})) N, !,
ring rmorphism-Z In1 OutM1 Out1 VM, !,
Expand Down
45 changes: 23 additions & 22 deletions theories/common.v
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
From elpi Require Import elpi.
From Coq Require Import QArith.
From Coq.micromega Require Import OrderedRing RingMicromega.
From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint.

Check warning on line 4 in theories/common.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:coq-dev) 

Hiding binding of key N to N_scope

Check warning on line 4 in theories/common.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:coq-dev) 

Hiding binding of key Z to Z_scope
Expand Down Expand Up @@ -1367,25 +1368,25 @@ Qed.

End RealField.

Import Instances.

Notation nat_nmodType := Datatypes_nat__canonical__CountRing_Nmodule.
Notation nat_semiRingType := Datatypes_nat__canonical__GRing_SemiRing.
Notation nat_comSemiRingType := Datatypes_nat__canonical__GRing_ComSemiRing.
Notation N_nmodType := BinNums_N__canonical__GRing_Nmodule.
Notation N_semiRingType := BinNums_N__canonical__GRing_SemiRing.
Notation N_comSemiRingType := BinNums_N__canonical__GRing_ComSemiRing.
Notation int_nmodType := ssrint_int__canonical__GRing_Nmodule.
Notation int_zmodType := ssrint_int__canonical__GRing_Zmodule.
Notation int_semiRingType := ssrint_int__canonical__GRing_SemiRing.
Notation int_ringType := ssrint_int__canonical__GRing_Ring.
Notation int_comRingType := ssrint_int__canonical__GRing_ComRing.
Notation int_unitRingType := ssrint_int__canonical__GRing_UnitRing.
Notation Z_nmodType := BinNums_Z__canonical__GRing_Nmodule.
Notation Z_zmodType := BinNums_Z__canonical__GRing_Zmodule.
Notation Z_semiRingType := BinNums_Z__canonical__GRing_SemiRing.
Notation Z_ringType := BinNums_Z__canonical__GRing_Ring.
Notation Z_comRingType := BinNums_Z__canonical__GRing_ComRing.
Notation Z_unitRingType := BinNums_Z__canonical__GRing_UnitRing.

Notation GRing_Zmodule__to__GRing_Nmodule := GRing_Zmodule__to__GRing_Nmodule.
Elpi Db canonicals.db lp:{{

pred canonical-nat-nmodule o:constant.
pred canonical-nat-semiring o:constant.
pred canonical-nat-comsemiring o:constant.
pred canonical-N-nmodule o:constant.
pred canonical-N-semiring o:constant.
pred canonical-N-comsemiring o:constant.
pred canonical-int-nmodule o:constant.
pred canonical-int-zmodule o:constant.
pred canonical-int-semiring o:constant.
pred canonical-int-ring o:constant.
pred canonical-int-comring o:constant.
pred canonical-int-unitring o:constant.
pred canonical-Z-nmodule o:constant.
pred canonical-Z-zmodule o:constant.
pred canonical-Z-semiring o:constant.
pred canonical-Z-ring o:constant.
pred canonical-Z-comring o:constant.
pred canonical-Z-unitring o:constant.

}}.
24 changes: 12 additions & 12 deletions theories/lra.elpi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -274,25 +274,25 @@ pred nmod.additive i:bool, i:term, i:additive, i:term -> term, i:term, i:term,
o:term, o:term, o:list term.
nmod.additive Inv V (additive U _ Morph) NewMorph NewMorphInst In1
{{ @MnatAdditive lp:U lp:NewMorphInst lp:OutM1 }} Out VM :-
coq.unify-eq V {{ nat_nmodType }} ok,
coq.unify-eq V (global (const { canonical-nat-nmodule })) ok,
mem VM { cond-inv Inv (Morph (NewMorph {{ 1%N }})) } N, !,
ring Inv rmorphism-nat In1 OutM1 Out1 VM, !,
build.mul { build.variable { positive-constant {calc (N + 1)} } } Out1 Out.
nmod.additive Inv V (additive U _ Morph) NewMorph NewMorphInst In1
{{ @MNAdditive lp:U lp:NewMorphInst lp:OutM1 }} Out VM :-
coq.unify-eq V {{ N_nmodType }} ok,
coq.unify-eq V (global (const { canonical-N-nmodule })) ok,
mem VM { cond-inv Inv (Morph (NewMorph {{ 1%num }})) } N, !,
ring Inv rmorphism-N In1 OutM1 Out1 VM, !,
build.mul { build.variable { positive-constant {calc (N + 1)} } } Out1 Out.
nmod.additive Inv V (additive U _ Morph) NewMorph NewMorphInst In1
{{ @MintAdditive lp:U lp:NewMorphInst lp:OutM1 }} Out VM :-
coq.unify-eq V {{ int_nmodType }} ok,
coq.unify-eq V (global (const { canonical-int-nmodule })) ok,
mem VM { cond-inv Inv (Morph (NewMorph {{ 1%Z }})) } N, !,
ring Inv rmorphism-int In1 OutM1 Out1 VM, !,
build.mul { build.variable { positive-constant {calc (N + 1)} } } Out1 Out.
nmod.additive Inv V (additive U _ Morph) NewMorph NewMorphInst In1
{{ @MZAdditive lp:U lp:NewMorphInst lp:OutM1 }} Out VM :-
coq.unify-eq V {{ Z_nmodType }} ok,
coq.unify-eq V (global (const { canonical-Z-nmodule })) ok,
mem VM { cond-inv Inv (Morph (NewMorph {{ Zpos 1 }})) } N, !,
ring Inv rmorphism-Z In1 OutM1 Out1 VM, !,
build.mul { build.variable { positive-constant {calc (N + 1)} } } Out1 Out.
Expand Down Expand Up @@ -536,22 +536,22 @@ pred ring.rmorphism i:bool, i:term, i:rmorphism, i:term -> term, i:term, i:term,
o:term, o:term, o:list term.
ring.rmorphism Inv S C _ NewMorphInst In1
{{ @RnatMorph lp:R lp:NewMorphInst lp:OutM1 }} Out1 VM :-
coq.unify-eq S {{ nat_semiRingType }} ok, !,
coq.unify-eq S (global (const { canonical-nat-semiring })) ok, !,
rmorphism->sring C R, !,
ring Inv rmorphism-nat In1 OutM1 Out1 VM.
ring.rmorphism Inv S C _ NewMorphInst In1
{{ @RNMorph lp:R lp:NewMorphInst lp:OutM1 }} Out1 VM :-
coq.unify-eq S {{ N_semiRingType }} ok, !,
coq.unify-eq S (global (const { canonical-N-semiring })) ok, !,
rmorphism->sring C R, !,
ring Inv rmorphism-N In1 OutM1 Out1 VM.
ring.rmorphism Inv S C _ NewMorphInst In1
{{ @RintMorph lp:R lp:NewMorphInst lp:OutM1 }} Out1 VM :-
coq.unify-eq S {{ int_semiRingType }} ok, !,
coq.unify-eq S (global (const { canonical-int-semiring })) ok, !,
rmorphism->sring C R, !,
ring Inv rmorphism-int In1 OutM1 Out1 VM.
ring.rmorphism Inv S C _ NewMorphInst In1
{{ @RZMorph lp:R lp:NewMorphInst lp:OutM1 }} Out1 VM :-
coq.unify-eq S {{ Z_semiRingType }} ok, !,
coq.unify-eq S (global (const { canonical-Z-semiring })) ok, !,
rmorphism->sring C R, !,
ring Inv rmorphism-Z In1 OutM1 Out1 VM.
ring.rmorphism Inv S C NewMorph NewMorphInst In1
Expand All @@ -565,28 +565,28 @@ pred ring.additive i:bool, i:term, i:rmorphism, i:term -> term, i:term, i:term,
o:term, o:term, o:list term.
ring.additive Inv V C NewMorph NewMorphInst In1
{{ @RnatAdditive lp:R lp:NewMorphInst lp:OutM1 }} Out VM :-
coq.unify-eq V {{ nat_nmodType }} ok,
coq.unify-eq V (global (const { canonical-nat-nmodule })) ok,
rmorphism->sring C R, rmorphism->morph C Morph,
mem VM { cond-inv Inv (Morph (NewMorph {{ 1%N }})) } N, !,
ring Inv rmorphism-nat In1 OutM1 Out1 VM, !,
build.mul { build.variable { positive-constant {calc (N + 1)} } } Out1 Out.
ring.additive Inv V C NewMorph NewMorphInst In1
{{ @RNAdditive lp:R lp:NewMorphInst lp:OutM1 }} Out VM :-
coq.unify-eq V {{ N_nmodType }} ok,
coq.unify-eq V (global (const { canonical-N-nmodule })) ok,
rmorphism->sring C R, rmorphism->morph C Morph,
mem VM { cond-inv Inv (Morph (NewMorph {{ 1%num }})) } N, !,
ring Inv rmorphism-N In1 OutM1 Out1 VM, !,
build.mul { build.variable { positive-constant {calc (N + 1)} } } Out1 Out.
ring.additive Inv V C NewMorph NewMorphInst In1
{{ @RintAdditive lp:R lp:NewMorphInst lp:OutM1 }} Out VM :-
coq.unify-eq V {{ int_nmodType }} ok,
coq.unify-eq V (global (const { canonical-int-nmodule })) ok,
rmorphism->sring C R, rmorphism->morph C Morph,
mem VM { cond-inv Inv (Morph (NewMorph {{ 1%Z }})) } N, !,
ring Inv rmorphism-int In1 OutM1 Out1 VM, !,
build.mul { build.variable { positive-constant {calc (N + 1)} } } Out1 Out.
ring.additive Inv V C NewMorph NewMorphInst In1
{{ @RZAdditive lp:R lp:NewMorphInst lp:OutM1 }} Out VM :-
coq.unify-eq V {{ Z_nmodType }} ok,
coq.unify-eq V (global (const { canonical-Z-nmodule })) ok,
rmorphism->sring C R, rmorphism->morph C Morph,
mem VM { cond-inv Inv (Morph (NewMorph {{ Zpos 1 }})) } N, !,
ring Inv rmorphism-Z In1 OutM1 Out1 VM, !,
Expand Down
3 changes: 3 additions & 0 deletions theories/lra.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -392,6 +392,7 @@ Strategy expand [Reval_formula Rnorm_formula Fnorm_formula].
Strategy expand [Reval_PFormula Feval_PFormula].

Elpi Tactic lra.
Elpi Accumulate Db canonicals.db.
Elpi Accumulate File common lra.
Elpi Typecheck.

Expand All @@ -400,3 +401,5 @@ Tactic Notation "nra" := elpi lra "nra_witness" "tacF" "tacR" 0.
Tactic Notation "psatz" integer(n) :=
elpi lra "psatz_witness" "tacF" "tacR" ltac_int:(n).
Tactic Notation "psatz" := elpi lra "psatz_witness" "tacF" "tacR" (-1).

Elpi Query lp:{{ canonical-init library "canonicals.db" }}.
Loading

0 comments on commit 1bb41b4

Please sign in to comment.