/usr/share/why3/drivers/coq-ssreflect.drv is in why3 0.88.3-1ubuntu4.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 | prelude "(* This file is generated by Why3's coq-ssreflect driver *)"
prelude "(* Beware! Only edit allowed sections below *)"
printer "coq-ssr"
filename "%t.v"
valid 0
unknown "Error: \\(.*\\)$" "\\1"
fail "Syntax error: \\(.*\\)$" "\\1"
time "why3cpulimit time : %s s"
transformation "inline_trivial"
transformation "eliminate_non_struct_recursion"
transformation "eliminate_if"
transformation "eliminate_non_lambda_set_epsilon"
transformation "eliminate_projections"
transformation "simplify_formula"
theory BuiltIn
prelude "
Require Import ssreflect ssrbool ssrfun ssrnat seq eqtype ssrint.
Require Import ssrint ssrwhy3.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
"
syntax type int "int"
syntax type real "R"
syntax predicate (=) "(%1 = %2)"
end
theory HighOrd
syntax type func "(%1 -> %2)"
syntax type pred "(%1 -> bool)"
syntax function (@) "(%1 %2)"
end
theory Bool
syntax type bool "bool"
syntax function True "true"
syntax function False "false"
end
theory bool.Bool
syntax function andb "(Init.Datatypes.andb %1 %2)"
syntax function orb "(Init.Datatypes.orb %1 %2)"
syntax function xorb "(Init.Datatypes.xorb %1 %2)"
syntax function notb "(Init.Datatypes.negb %1)"
syntax function implb "(Init.Datatypes.implb %1 %2)"
end
theory map.Map
syntax type map "(%1 -> %2)%type"
syntax function get "(%1 %2)"
end
theory map.Const
remove prop Const
end
theory int.Int
prelude "
Require Import ssralg ssrnum.
Import GRing.Theory Num.Theory.
Local Open Scope ring_scope."
syntax function zero "0%:Z"
syntax function one "1%:Z"
syntax function (+) "(%1 + %2)%R"
syntax function (-) "(%1 - %2)%R"
syntax function ( * ) "(%1 * %2)%R"
syntax function (-_) "(-%1)%R"
syntax predicate (<=) "(%1 <= %2)%R"
syntax predicate (<) "(%1 < %2)%R"
syntax predicate (>=) "(%1 >= %2)%R"
syntax predicate (>) "(%1 > %2)%R"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
remove prop CommutativeGroup.Unit_def_l
remove prop CommutativeGroup.Unit_def_r
remove prop CommutativeGroup.Inv_def_l
remove prop CommutativeGroup.Inv_def_r
remove prop Assoc.Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm.Comm
remove prop Unitary
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop CompatOrderMult
remove prop ZeroLessOne
end
theory array.Array
syntax type array "(array %1)"
syntax function get "(get %1 %2)"
syntax function length "(size %1 : int)"
syntax function elts "(get %1)"
syntax function set "(set %1 %2 %3)"
(* does not exist anymore
syntax function make "(make %1 %2)"
*)
end
theory matrix.Matrix
syntax type matrix "(matrix %1)"
syntax function get "(matrix_get %1 %2 %3)"
syntax function rows "(nrows %1 : int)"
syntax function columns "(ncols %1 : int)"
syntax function elts "(matrix_get_curry %1)"
syntax function set "(matrix_set %1 %2 %3)"
(* does not exist anymore
syntax function make "(matrix_make %1 %2)"
*)
end
|