EasyCrypt / easycrypt

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

New tactic: "proc case" #500

Closed strub closed 9 months ago

mbbarbosa commented 11 months ago

New use case: would be super useful if this also works when we have

lv <- (e1,...,en)

Unfolded as

lv.1 <- e1 ... lv.n <- en

fdupress commented 11 months ago

This is currently not valid EC, so we'd need to figure out a meaning for

lv.`1 <- e

First.

strub commented 11 months ago

This raises the question of having more general left-values.