search

EasyCrypt / easycrypt

EasyCrypt: Computer-Aided Cryptographic Proofs
MIT License
321 stars 49 forks source link

Anomaly #463

Closed strub closed 1 year ago

strub commented 1 year ago

Reported by Adrien Koutsos:

The following program causes an anomaly:

lemma foo : let x = 0 in x = 0.
proof.
  move=> x.
  have A : x = 0; 1: auto.
  have B : x = x; 1: auto.
  rewrite -A in B.
strub commented 1 year ago

@akoutsos