diff options
author | Son Ho | 2022-11-15 15:23:16 +0100 |
---|---|---|
committer | Son HO | 2022-11-16 15:45:32 +0100 |
commit | bd5706896dec0a1aef1accdf51f93af00c5dc6fe (patch) | |
tree | 09dd5431d351c8ef894092ea25fd9d2af54d3d6e /tests/coq/misc/External__Opaque.v | |
parent | dbb5d549176edd60440e689fd28c529944bc6e51 (diff) |
Improve formatting
Diffstat (limited to 'tests/coq/misc/External__Opaque.v')
-rw-r--r-- | tests/coq/misc/External__Opaque.v | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/tests/coq/misc/External__Opaque.v b/tests/coq/misc/External__Opaque.v index 19111a37..93652450 100644 --- a/tests/coq/misc/External__Opaque.v +++ b/tests/coq/misc/External__Opaque.v @@ -4,33 +4,33 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. Local Open Scope Primitives_scope. -Require Export External__Types . -Import External__Types . -Module External__Opaque . +Require Export External__Types. +Import External__Types. +Module External__Opaque. (** [core::mem::swap] *) Axiom core_mem_swap_fwd : - forall(T : Type) , T -> T -> state -> result (state * unit) - . + forall(T : Type), T -> T -> state -> result (state * unit) +. (** [core::mem::swap] *) Axiom core_mem_swap_back0 : - forall(T : Type) , T -> T -> state -> state -> result (state * T) - . + forall(T : Type), T -> T -> state -> state -> result (state * T) +. (** [core::mem::swap] *) Axiom core_mem_swap_back1 : - forall(T : Type) , T -> T -> state -> state -> result (state * T) - . + forall(T : Type), T -> T -> state -> state -> result (state * T) +. (** [core::num::nonzero::NonZeroU32::{14}::new] *) Axiom core_num_nonzero_non_zero_u32_new_fwd : u32 -> state -> result (state * (option Core_num_nonzero_non_zero_u32_t)) - . +. (** [core::option::Option::{0}::unwrap] *) Axiom core_option_option_unwrap_fwd : - forall(T : Type) , option T -> state -> result (state * T) - . + forall(T : Type), option T -> state -> result (state * T) +. End External__Opaque . |