Deducteam / lambdapi

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

Metavariable numbering not reset in each symbol/rule declaration #1097

Closed fblanqui closed 2 months ago

fblanqui commented 2 months ago

Metavariable numbering is not reset in each rule with with:

symbol A:TYPE;
symbol f:A → A → A;
debug +s;
rule f $x $y ↪ $x
with f $x $y ↪ $y;

ouputs:

debug +s
[file:///home/blanqui/src/lambdapi/tmp/1097.lp:5:7-9 ]
Pattern variable x can be replaced by a '_'.
[subj] f $0 $1 ↪ $1
[subj] replace pattern variables by metavariables: f ?1 ?3 ↪ ?3
[subj] LHS type: A
       LHS constraints: 
       f ?1 ?3 ↪ ?3
[subj] replace LHS metavariables by function symbols: f $1 $3 ↪ $3
[file:///home/blanqui/src/lambdapi/tmp/1097.lp:4:10-12 ]
Pattern variable y can be replaced by a '_'.
[subj] f $0 $1 ↪ $0
[subj] replace pattern variables by metavariables: f ?5 ?7 ↪ ?5
[subj] LHS type: A
       LHS constraints: 
       f ?5 ?7 ↪ ?5
[subj] replace LHS metavariables by function symbols: f $5 $7 ↪ $5
[file:///home/blanqui/src/lambdapi/tmp/1097.lp:4:0-5:18 ]
Unjoinable critical pair:
t ≔ f $0 $1
t ↪[] $0 ↪* $0
  with f $0' $1' ↪ $0'
t ↪[] $1 ↪* $1
  with f $0 $1 ↪ $1
fblanqui commented 2 months ago

fixed in #1099

fblanqui commented 2 months ago

@nicomarg should be helpful for you! ;-)