diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-03-02 18:06:18 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-03-02 18:06:18 +0000 |
| commit | c2ba535604cef5bc86369512e6f3c2833753a55a (patch) | |
| tree | fd0b83022443a3806a5bac4e82299c513f5d2f8d /src/common/Show.v | |
| parent | 88d015ba178665ee21b282f364ccf047522e3b1c (diff) | |
| download | vericert-c2ba535604cef5bc86369512e6f3c2833753a55a.tar.gz vericert-c2ba535604cef5bc86369512e6f3c2833753a55a.zip | |
Update Coq version to 8.14.1
Diffstat (limited to 'src/common/Show.v')
| -rw-r--r-- | src/common/Show.v | 30 |
1 files changed, 10 insertions, 20 deletions
diff --git a/src/common/Show.v b/src/common/Show.v index 4c66725..20c07e7 100644 --- a/src/common/Show.v +++ b/src/common/Show.v @@ -1,4 +1,4 @@ -(* +(* * Vericert: Verified high-level synthesis. * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> * @@ -24,15 +24,11 @@ From Coq Require Import Local Open Scope string. -Class Show A : Type := - { - show : A -> string - }. +Class Show A : Type := { show : A -> string }. +#[export] Instance showBool : Show bool := - { - show := fun b:bool => if b then "true" else "false" - }. + { show := fun b:bool => if b then "true" else "false" }. Fixpoint string_of_nat_aux (time n : nat) (acc : string) : string := let d := match n mod 10 with @@ -52,17 +48,11 @@ Fixpoint string_of_nat_aux (time n : nat) (acc : string) : string := Definition string_of_nat (n : nat) : string := string_of_nat_aux n n "". -Instance showNat : Show nat := - { - show := string_of_nat - }. +#[export] +Instance showNat : Show nat := { show := string_of_nat }. -Instance showZ : Show Z := - { - show a := show (Z.to_nat a) - }. +#[export] +Instance showZ : Show Z := { show a := show (Z.to_nat a) }. -Instance showPositive : Show positive := - { - show a := show (Zpos a) - }. +#[export] +Instance showPositive : Show positive := { show a := show (Zpos a) }. |