Skip to content

Commit

Permalink
cleanup
Browse files Browse the repository at this point in the history
  • Loading branch information
@mbbarbosa-lectures
mbbarbosa-lectures committed Nov 6, 2024
1 parent 2ce5124 commit b83919e
Showing 1 changed file with 0 additions and 2 deletions.
2 changes: 0 additions & 2 deletions proof/correctness/avx2/MLKEM_InnerPKE_avx2.ec
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1776,8 +1776,6 @@ qed.

op init_768_16 (f: int -> W16.t) : W16.t Array768.t = Array768.init f.

print Array768.initE.

bind op [W16.t & Array768.t] init_768_16 "ainit".
realize bvainitP.
rewrite /init_768_16 => f.
Expand Down

0 comments on commit b83919e

Please sign in to comment.