Commit d4518463 authored by Francois Bobot's avatar Francois Bobot

correction of zsh completion and test of encoding instantiate

parent 334d3635
......@@ -29,7 +29,7 @@ _arguments -s -S \
"(-L --library -I)"'-I'"[same as -L (obsolete)]:Mlpost lib path (obsolete use -L):_files -/ "\
"(-D --driver -P -prover)"'-P'"[<prover> Prove or print (with -o) the selected goals]:<prover>:->provers"\
"(-D --driver -P -prover)"'--prover'"[same as -P]:<prover>:->provers"\
'-M'"[<meta_name>,<string> Add a meta option to each tasks]:<meta_name>:->metas:<meta_arg>:"\
'*-M'"[<meta_name> <string> Add a meta option to each tasks]:<meta_name>:->metas:<meta_arg>:"\
"(-F --format)"'-F'"[<format> Input format (default: \"why\")]:<input format>:"\
"(-F --format)"'--format'"[same as -F]:<input format>:"\
"(-t --timelimit)"'-t'"[<sec> Set the prover\'s time limit (default=10, no limit=0)]:<timeout s>:"\
......@@ -63,18 +63,20 @@ last_theory=$last_theories[-1]
case $state in
_message "<transformations>"
_message "<transformations>";
compadd $($cmd --list-transforms | grep -e "^ ");
return 0
_message "<provers>"
_message "<provers>";
compadd $($cmd --list-provers | egrep -E "^ [a-z]"|cut -d' ' -f 3);
return 0
_message "<metas>"
compadd "$($cmd --list-metas | egrep -E "^ [a-z]" | sed "s/^[ ]*\(.*\)$/'\1'/")";
_message "<metas>";
METAS="$($cmd --list-metas | egrep -E "^ [a-z]" | sed "s/^[ ]*//")";
compadd $METAS;
return 0
......@@ -72,10 +72,12 @@ theory TestEnco
logic p2(mytype 'a) : 'a
type toto
logic f (toto) : mytype toto
axiom A0 : forall x : toto. f(x) = p(x)
logic g (mytype int) : toto
logic h (int) : mytype toto
logic h (int) : toto
axiom A05 : forall x : int. g(p(x)) = h(x)
axiom A1 : forall x : mytype 'a. p(p2(x)) = x
goal G2 : forall x:int. f(g(p(x))) = h(x)
goal G2 : forall x:mytype toto. f(p2(x)) = x
theory TestIte
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