search

Deducteam / lambdapi

Proof assistant based on the λΠ-calculus modulo rewriting
Other
265 stars 35 forks source link

Fix issue #1001 #1087

Closed gabrielhdt closed 2 months ago

gabrielhdt commented 2 months ago

With the invaluable help of Michael Faerber

fblanqui commented 2 months ago

CI fails because iss1001.lp cannot be translated to dedukti. This seems to be a bug in lambdapi, file src/export/rawdk.ml, line 171:

  | [Commu;Assoc _], [Protec], [], [] -> out ppf "defac "

should be replaced by:

  | [Commu;Assoc _], [], [], [] -> out ppf "defac "
  | [Commu;Assoc _], [Protec], [], [] -> out ppf "private defac "
fblanqui commented 2 months ago

To be fixed in #1088 .

fblanqui commented 2 months ago

To be fixed in #1089