Nous avons procédé ce jeudi matin 08 avril 2021 à une MAJ de sécurité urgente. Nous sommes passé de la version 13.9.3 à la version 13.9.5 les releases notes correspondantes sont ici:
https://about.gitlab.com/releases/2021/03/17/security-release-gitlab-13-9-4-released/
https://about.gitlab.com/releases/2021/03/31/security-release-gitlab-13-10-1-released/

Commit 1140fb4f authored by MARCHE Claude's avatar MARCHE Claude

some basic transformations with arguments: case, cut, etc.

parent 062efb5b
open Trans
let rec dup n x = if n = 0 then [] else x::(dup (n-1) x)
let duplicate args task =
match args with
| [TAint n] -> dup n task
| _ -> failwith "wrong arguments for duplicate"
let case _t task = (* Sylvain *)
[task;task]
(* TODO : from task [delta |- G] , build the tasks [delta, t] |- G] and [delta, not t | - G] *)
let cut _t task = (* Sylvain *)
[task;task]
(* TODO : from task [delta |- G] , build the tasks [delta] |- t] and [delta, t | - G] *)
let exists _t task = (* ? *)
[task;task]
(* TODO : from task [delta |- exists x. G] , build the task [delta] |- G[x -> t]] *)
let remove _name task =
[task;task]
(* TODO :from task [delta, name:A |- G] build the task [delta |- G] *)
let simple_apply _name _t task = (* ? *)
[task;task]
(* TODO : from task [delta, name:forall x.A |- G,
build the task [delta,name:forall x.A,name':A[x -> t]] |- G] *)
let apply _name task = (* ? *)
[task;task]
(* TODO : from task [delta, name:forall x.A->B |- G,
build the task [delta,name:forall x.A->B] |- A[x -> t]] ou t est tel que B[x->t] = G *)
let case' args task =
match args with
| [TAterm t] -> case t task
| _ -> failwith "wrong arguments for case"
let () = register_transform_with_args ~desc:"test case" "case" case'
let () = register_transform_with_args ~desc:"test duplicate" "duplicate" duplicate
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