search

mit-plv / fiat-crypto

Cryptographic Primitive Code Generation by Fiat
http://adam.chlipala.net/papers/FiatCryptoSP19/FiatCryptoSP19.pdf
Other
717 stars 147 forks source link

Fix typos #1860

Closed atrieu closed 7 months ago

atrieu commented 7 months ago

Before,

field_parameters_prefixed =
fun (M_pos : positive) (a24 : F M_pos) (prefix : string) =>
{|
 (* ... *)
  select_znz := prefix ++ "felem_copy";
  felem_copy := prefix ++ "small_literal";
  from_word := prefix ++ "select_znz"
|}
     : forall M_pos : positive, F M_pos -> string -> FieldParameters

After,

field_parameters_prefixed =
fun (M_pos : positive) (a24 : F M_pos) (prefix : string) =>
{|
 (* ... *)
  select_znz := prefix ++ "select_znz";
  felem_copy := prefix ++ "felem_copy";
  from_word := prefix ++ "from_word"
|}
     : forall M_pos : positive, F M_pos -> string -> FieldParameters