Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit 33e76ab2 authored by Francois Bobot's avatar Francois Bobot

ajout de algebra

parent 9bd8f1b8
......@@ -114,3 +114,7 @@ echo "=== Type-checking good files ==="
goods typing/good --type-only
echo ""
echo "=== Type-checking lib/prelude ==="
goods ../lib/prelude --type-only
echo ""
theory AC
type t
logic op(t,t) : t
axiom Comm : forall x,y:t. op(x,y) = op(y,x)
axiom Assoc : forall x,y,z:t. op(op(x,y),z)=op(x,op(y,z))
end
theory Group
type t
logic neutral : t
logic op(t,t) : t
logic inv(t) : t
axiom Neutral_def : forall x:t. op(x,neutral) = x
clone AC with type t = t,
logic op = op
axiom Inv_def : forall x:t. op(x,inv(x)) = neutral
end
\ No newline at end of file
......@@ -124,3 +124,8 @@ let elt_of_oelt ~ty ~logic ~prop ~use ~clone d =
| Dprop p -> prop p
| Duse th -> use th
| Dclone c -> clone c
let fold_context_of_decl f ctxt env ctxt_done d =
let env,decls = f ctxt env d in
env,List.fold_left add_decl ctxt_done decls
......@@ -76,3 +76,9 @@ val elt_of_oelt :
use:(theory -> decl list) ->
clone:((ident * ident) list -> decl list) ->
(decl -> decl list)
val fold_context_of_decl:
(context -> 'a -> decl -> 'a * decl list) ->
context -> 'a -> context -> decl -> ('a * context)
......@@ -47,6 +47,7 @@ let () =
(fun f -> files := f :: !files)
"usage: why [options] files..."
let in_emacs = Sys.getenv "TERM" = "dumb"
let transform = !transform || !simplify_recursive || !inlining
let rec report fmt = function
......@@ -61,8 +62,12 @@ let rec report fmt = function
| Context.UnknownIdent i ->
fprintf fmt "anomaly: unknownident %s" i.Ident.id_short
| e ->
fprintf fmt "anomaly: %s" (Printexc.to_string e)
if in_emacs then
let dir = Filename.dirname (Filename.dirname Sys.executable_name) in
fprintf fmt "Entering directory `%s'@\n" dir;
fprintf fmt "anomaly:@\n%s" (Printexc.to_string e)
else
fprintf fmt "anomaly: %s" (Printexc.to_string e)
let type_file env file =
let c = open_in file in
let lb = Lexing.from_channel c in
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment