Rename op to uniop because it conflicts with Isabelle's op.

lem/evm.lem

@@ -1178,8 +1178,8 @@ end
 val jump : variable_ctx -> constant_ctx -> instruction_result
 let jump v c = match v.vctx_stack with
  | [] -> instruction_failure_result v [TooShortStack]
- | pos :: tl ->
-     let v_new = <| v with vctx_stack = tl; vctx_pc = uint pos |> in
+ | pos :: tail ->
+     let v_new = <| v with vctx_stack = tail; vctx_pc = uint pos |> in
      match vctx_next_instruction v_new c with
       | Just (Pc JUMPDEST) -> InstructionContinue v_new
       | _ -> instruction_failure_result v [InvalidJumpDestination]
@@ -1431,7 +1431,7 @@ let stop v _ =
 (* POP removes the topmost element of the stack: *)
 val pop : variable_ctx -> constant_ctx -> instruction_result
 let pop v c = match v.vctx_stack with
- | _ :: tl -> InstructionContinue (vctx_advance_pc c <| v with vctx_stack = tl |>)
+ | _ :: tail -> InstructionContinue (vctx_advance_pc c <| v with vctx_stack = tail |>)
  | [] -> instruction_failure_result v [TooShortStack]
 end
 
@@ -1986,7 +1986,7 @@ end
 
 val account_state_pop_ongoing_call : account_state -> account_state
 let account_state_pop_ongoing_call orig = match orig.account_ongoing_calls with
- | _ :: tl -> <| orig with account_ongoing_calls = tl |>
+ | _ :: tail -> <| orig with account_ongoing_calls = tail |>
  | _ -> <| orig with account_ongoing_calls = [] |>
 end
 

lem/word160.lem

@@ -39,7 +39,7 @@ val word160NatOp : (bitSequence -> nat -> bitSequence) -> word160 -> nat -> word
 let word160NatOp binop w1 n = bs_to_w160 (binop (w160_to_bs w1) n)
 
 val word160UnaryOp : (bitSequence -> bitSequence) -> word160 -> word160
-let word160UnaryOp op w = bs_to_w160 (op (w160_to_bs w))
+let word160UnaryOp uniop w = bs_to_w160 (uniop (w160_to_bs w))
 
 val word160ToInteger : word160 -> integer
 let word160ToInteger w = integerFromBitSeq (w160_to_bs w)

lem/word256.lem

@@ -43,7 +43,7 @@ val word256NatOp : (bitSequence -> nat -> bitSequence) -> word256 -> nat -> word
 let word256NatOp binop w1 n = bs_to_w256 (binop (w256_to_bs w1) n)
 
 val word256UnaryOp : (bitSequence -> bitSequence) -> word256 -> word256
-let word256UnaryOp op w = bs_to_w256 (op (w256_to_bs w))
+let word256UnaryOp uniop w = bs_to_w256 (uniop (w256_to_bs w))
 
 val size256 : integer
 let size256 = 2 ** 256

lem/word32.lem

@@ -40,7 +40,7 @@ val word32NatOp : (bitSequence -> nat -> bitSequence) -> word32 -> nat -> word32
 let word32NatOp binop w1 n = bs_to_w32 (binop (w32_to_bs w1) n)
 
 val word32UnaryOp : (bitSequence -> bitSequence) -> word32 -> word32
-let word32UnaryOp op w = bs_to_w32 (op (w32_to_bs w))
+let word32UnaryOp uniop w = bs_to_w32 (uniop (w32_to_bs w))
 
 val size32 : integer
 let size32 = 2 ** 32

lem/word4.lem

@@ -39,7 +39,7 @@ val word4NatOp : (bitSequence -> nat -> bitSequence) -> word4 -> nat -> word4
 let word4NatOp binop w1 n = bs_to_w4 (binop (w4_to_bs w1) n)
 
 val word4UnaryOp : (bitSequence -> bitSequence) -> word4 -> word4
-let word4UnaryOp op w = bs_to_w4 (op (w4_to_bs w))
+let word4UnaryOp uniop w = bs_to_w4 (uniop (w4_to_bs w))
 
 val word4ToNat : word4 -> nat
 let word4ToNat w = natFromInt (intFromInteger (integerFromBitSeq (w4_to_bs w)) mod 16)

lem/word64.lem

@@ -42,7 +42,7 @@ val word64NatOp : (bitSequence -> nat -> bitSequence) -> word64 -> nat -> word64
 let word64NatOp binop w1 n = bs_to_w64 (binop (w64_to_bs w1) n)
 
 val word64UnaryOp : (bitSequence -> bitSequence) -> word64 -> word64
-let word64UnaryOp op w = bs_to_w64 (op (w64_to_bs w))
+let word64UnaryOp uniop w = bs_to_w64 (uniop (w64_to_bs w))
 
 val size64 : integer
 let size64 = 2 ** 64

lem/word8.lem

@@ -39,7 +39,7 @@ val word8NatOp : (bitSequence -> nat -> bitSequence) -> word8 -> nat -> word8
 let word8NatOp binop w1 n = bs_to_w8 (binop (w8_to_bs w1) n)
 
 val word8UnaryOp : (bitSequence -> bitSequence) -> word8 -> word8
-let word8UnaryOp op w = bs_to_w8 (op (w8_to_bs w))
+let word8UnaryOp uniop w = bs_to_w8 (uniop (w8_to_bs w))
 
 val word8ToNat : word8 -> nat
 let word8ToNat w = natFromInt (intFromInteger (integerFromBitSeq (w8_to_bs w)) mod 256)