diff options
Diffstat (limited to 'src/versions/standard/Structures_standard.v')
| -rw-r--r-- | src/versions/standard/Structures_standard.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/src/versions/standard/Structures_standard.v b/src/versions/standard/Structures_standard.v index 04b396f..4894ebd 100644 --- a/src/versions/standard/Structures_standard.v +++ b/src/versions/standard/Structures_standard.v @@ -1,3 +1,15 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2019 *) +(* *) +(* See file "AUTHORS" for the list of authors *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + + Require Import Int63. Require Import List. @@ -7,6 +19,9 @@ Section Trace. Definition trace (step:Type) := ((list step) * step)%type. + Definition trace_to_list {step:Type} (t:trace step) : list step := + let (t, _) := t in t. + Definition trace_length {step:Type} (t:trace step) : int := let (t,_) := t in List.fold_left (fun i _ => (i+1)%int) t 0%int. @@ -33,3 +48,8 @@ Section Trace. Admitted. End Trace. + + +Definition nat_eqb := Nat.eqb. +Definition nat_eqb_eq := Nat.eqb_eq. +Definition nat_eqb_refl := Nat.eqb_refl. |