diff --git a/.nojekyll b/.nojekyll
new file mode 100644
index 0000000..e69de29
diff --git a/docs/coqdoc/ABS.abs_defs.html b/docs/coqdoc/ABS.abs_defs.html
new file mode 100644
index 0000000..6d9297d
--- /dev/null
+++ b/docs/coqdoc/ABS.abs_defs.html
@@ -0,0 +1,212 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
Definition i :
Set :=
nat.
+
Lemma eq_i:
forall (
x y :
i),
{x = y} + {x <> y}.
+
Proof.
+
decide equality;
auto with ott_coq_equality arith.
+
Defined.
+
Hint Resolve eq_i :
ott_coq_equality.
+
Definition fn :
Set :=
string.
+
Lemma eq_fn:
forall (
x y :
fn),
{x = y} + {x <> y}.
+
Proof.
+
decide equality;
auto with ott_coq_equality arith.
+
Defined.
+
Hint Resolve eq_fn :
ott_coq_equality.
+
Definition x :
Set :=
string.
+
Lemma eq_x:
forall (
x' y :
x),
{x' = y} + {x' <> y}.
+
Proof.
+
decide equality;
auto with ott_coq_equality arith.
+
Defined.
+
Hint Resolve eq_x :
ott_coq_equality.
+
Definition b :
Set :=
bool.
+
Lemma eq_b:
forall (
x y :
b),
{x = y} + {x <> y}.
+
Proof.
+
decide equality;
auto with ott_coq_equality arith.
+
Defined.
+
Hint Resolve eq_b :
ott_coq_equality.
+
Definition z :
Set :=
Z.
+
Lemma eq_z:
forall (
x y :
z),
{x = y} + {x <> y}.
+
Proof.
+
decide equality;
auto with ott_coq_equality arith.
+
Defined.
+
Hint Resolve eq_z :
ott_coq_equality.
+
+
+
Inductive T :
Set :=
+ |
T_bool :
T
+ |
T_int :
T.
+
+
+
Inductive t :
Set :=
+ |
t_b (
b5:
b)
+ |
t_int (
z5:
z) .
+
+
+
Inductive sig :
Set :=
+ |
sig_sig (
_:
list T) (
T_5:
T).
+
+
+
Inductive e :
Set :=
+ |
e_t (
t5:
t)
+ |
e_var (
x5:
x)
+ |
e_fn_call (
fn5:
fn) (
_:
list e) .
+
+
+
Inductive ctxv :
Set :=
+ |
ctxv_T (
T5:
T)
+ |
ctxv_sig (
sig5:
sig).
+
+
+
Inductive F :
Set :=
+ |
F_fn (
T_5:
T) (
fn5:
fn) (
_:
list (
T*x)) (
e5:
e).
+
+
+
Definition s :
Type :=
Map.t t.
+
+
+
Definition G :
Type :=
Map.t ctxv.
+
+
+
+induction principles
+
+
+
+
+definitions
+
+
+
+
+
+
Inductive typ_e :
G -> e -> T -> Prop :=
+ |
typ_bool :
forall (
G5:
G) (
b5:
b),
+
typ_e G5 (
e_t (
t_b b5))
T_bool
+ |
typ_int :
forall (
G5:
G) (
z5:
z),
+
typ_e G5 (
e_t (
t_int z5))
T_int
+ |
typ_var :
forall (
G5:
G) (
x5:
x) (
T5:
T),
+
(Map.find x5 G5 = Some (
ctxv_T T5 )
) ->
+
typ_e G5 (
e_var x5)
T5
+ |
typ_func_expr :
forall (
e_T_list:
list (
e*T)) (
G5:
G) (
fn5:
fn) (
T_5:
T),
+
(forall e_ T_,
In (e_,T_) (
map (
fun (
pat_: (
e*T)) =>
match pat_ with (e_,T_) =>
(e_,T_) end)
e_T_list)
-> (typ_e G5 e_ T_)) ->
+
(Map.find fn5 G5 = Some (
ctxv_sig (
sig_sig (
map (
fun (
pat_:(
e*T)) =>
match pat_ with (e_,T_) =>
T_ end )
e_T_list)
T_5) )
) ->
+
typ_e G5 (
e_fn_call fn5 (
map (
fun (
pat_:(
e*T)) =>
match pat_ with (e_,T_) =>
e_ end )
e_T_list))
T_5
+
with typ_F :
G -> F -> Prop :=
+ |
typ_func_decl :
forall (
T_x_list:
list (
T*x)) (
G5:
G) (
T_5:
T) (
fn5:
fn) (
e5:
e),
+
(Map.find fn5 G5 = Some (
ctxv_sig (
sig_sig (
map (
fun (
pat_:(
T*x)) =>
match pat_ with (T_,x_) =>
T_ end )
T_x_list)
T_5) )
) ->
+
typ_e (
fold_right (
fun (
ax :
x * T) (
G5 :
G) =>
Map.add (
fst ax) (
ctxv_T (
snd ax))
G5)
G5 (
map (
fun (
pat_:(
T*x)) =>
match pat_ with (T_,x_) =>
(x_,T_) end )
T_x_list) )
e5 T_5 ->
+
typ_F G5 (
F_fn T_5 fn5 T_x_list e5).
+
+
+
+definitions
+
+
+
+
+
+
Inductive red_e :
list F -> s -> e -> s -> e -> Prop :=
+ |
red_var :
forall (
F_list:
list F) (
s5:
s) (
x5:
x) (
t5:
t),
+
(Map.find x5 s5 = Some (
t5 )
) ->
+
red_e F_list s5 (
e_var x5)
s5 (
e_t t5)
+ |
red_fun_exp :
forall (
e'_list e_list:
list e) (
F_list:
list F) (
s5:
s) (
fn5:
fn) (
e_5:
e) (
s':
s) (
e':
e),
+
red_e F_list s5 e_5 s' e' ->
+
red_e F_list s5 (
e_fn_call fn5 ((
app e_list (
app (
cons e_5 nil) (
app e'_list nil)))))
s' (
e_fn_call fn5 ((
app e_list (
app (
cons e' nil) (
app e'_list nil)))))
+ |
red_fun_ground :
forall (
T_x_t_y_list:
list (
T*x*t*x)) (
F'_list F_list:
list F) (
T_5:
T) (
fn5:
fn) (
e5:
e) (
s5:
s),
+
True ->
+
red_e ((
app F_list (
app (
cons (
F_fn T_5 fn5 (
map (
fun (
pat_:(
T*x*t*x)) =>
match pat_ with (T_,x_,t_,y_) =>
(T_,x_) end )
T_x_t_y_list)
e5)
nil) (
app F'_list nil))))
s5 (
e_fn_call fn5 (
map (
fun (
pat_:(
T*x*t*x)) =>
match pat_ with (T_,x_,t_,y_) => (
e_t t_)
end )
T_x_t_y_list)) (
fold_right (
fun (
xt :
x * t) (
s5 :
s) =>
Map.add (
fst xt) (
snd xt)
s5)
s5 (
map (
fun (
pat_:(
T*x*t*x)) =>
match pat_ with (T_,x_,t_,y_) =>
(y_,t_) end )
T_x_t_y_list) ) (
e5 ) .
+
+
+
+
+
+
+
+
+
+
+
ABS Functional Metatheory
+
+
+
+
+
+
+
+
+
+| Global Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(85 entries) |
+
+
+| Module Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(1 entry) |
+
+
+| Variable Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(7 entries) |
+
+
+| Library Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(2 entries) |
+
+
+| Constructor Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(19 entries) |
+
+
+| Lemma Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(6 entries) |
+
+
+| Inductive Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(9 entries) |
+
+
+| Section Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(1 entry) |
+
+
+| Definition Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(40 entries) |
+
+
+
+
Global Index
+
A
+
abs_functional_metatheory [library]
+
abs_defs [library]
+
B
+
b [definition, in
ABS.abs_defs]
+
C
+
ctxv [inductive, in
ABS.abs_defs]
+
ctxv_sind [definition, in
ABS.abs_defs]
+
ctxv_rec [definition, in
ABS.abs_defs]
+
ctxv_ind [definition, in
ABS.abs_defs]
+
ctxv_rect [definition, in
ABS.abs_defs]
+
ctxv_sig [constructor, in
ABS.abs_defs]
+
ctxv_T [constructor, in
ABS.abs_defs]
+
E
+
e [inductive, in
ABS.abs_defs]
+
eq_z [lemma, in
ABS.abs_defs]
+
eq_b [lemma, in
ABS.abs_defs]
+
eq_x [lemma, in
ABS.abs_defs]
+
eq_fn [lemma, in
ABS.abs_defs]
+
eq_i [lemma, in
ABS.abs_defs]
+
e_ott_ind [definition, in
ABS.abs_defs]
+
e_rect.H_list_e_cons [variable, in
ABS.abs_defs]
+
e_rect.H_list_e_nil [variable, in
ABS.abs_defs]
+
e_rect.H_e_fn_call [variable, in
ABS.abs_defs]
+
e_rect.H_e_var [variable, in
ABS.abs_defs]
+
e_rect.H_e_t [variable, in
ABS.abs_defs]
+
e_rect.P_list_e [variable, in
ABS.abs_defs]
+
e_rect.P_e [variable, in
ABS.abs_defs]
+
e_rect [section, in
ABS.abs_defs]
+
e_sind [definition, in
ABS.abs_defs]
+
e_rec [definition, in
ABS.abs_defs]
+
e_ind [definition, in
ABS.abs_defs]
+
e_rect [definition, in
ABS.abs_defs]
+
e_fn_call [constructor, in
ABS.abs_defs]
+
e_var [constructor, in
ABS.abs_defs]
+
e_t [constructor, in
ABS.abs_defs]
+
F
+
F [inductive, in
ABS.abs_defs]
+
fn [definition, in
ABS.abs_defs]
+
F_sind [definition, in
ABS.abs_defs]
+
F_rec [definition, in
ABS.abs_defs]
+
F_ind [definition, in
ABS.abs_defs]
+
F_rect [definition, in
ABS.abs_defs]
+
F_fn [constructor, in
ABS.abs_defs]
+
G
+
G [definition, in
ABS.abs_defs]
+
G_vdash_s [definition, in
ABS.abs_functional_metatheory]
+
I
+
i [definition, in
ABS.abs_defs]
+
M
+
Map [module, in
ABS.abs_defs]
+
R
+
red_e_sind [definition, in
ABS.abs_defs]
+
red_e_ind [definition, in
ABS.abs_defs]
+
red_fun_ground [constructor, in
ABS.abs_defs]
+
red_fun_exp [constructor, in
ABS.abs_defs]
+
red_var [constructor, in
ABS.abs_defs]
+
red_e [inductive, in
ABS.abs_defs]
+
S
+
s [definition, in
ABS.abs_defs]
+
sig [inductive, in
ABS.abs_defs]
+
sig_sind [definition, in
ABS.abs_defs]
+
sig_rec [definition, in
ABS.abs_defs]
+
sig_ind [definition, in
ABS.abs_defs]
+
sig_rect [definition, in
ABS.abs_defs]
+
sig_sig [constructor, in
ABS.abs_defs]
+
subG [definition, in
ABS.abs_functional_metatheory]
+
T
+
t [inductive, in
ABS.abs_defs]
+
T [inductive, in
ABS.abs_defs]
+
type_preservation [lemma, in
ABS.abs_functional_metatheory]
+
typ_F_sind [definition, in
ABS.abs_defs]
+
typ_F_ind [definition, in
ABS.abs_defs]
+
typ_e_sind [definition, in
ABS.abs_defs]
+
typ_e_ind [definition, in
ABS.abs_defs]
+
typ_func_decl [constructor, in
ABS.abs_defs]
+
typ_F [inductive, in
ABS.abs_defs]
+
typ_func_expr [constructor, in
ABS.abs_defs]
+
typ_var [constructor, in
ABS.abs_defs]
+
typ_int [constructor, in
ABS.abs_defs]
+
typ_bool [constructor, in
ABS.abs_defs]
+
typ_e [inductive, in
ABS.abs_defs]
+
t_sind [definition, in
ABS.abs_defs]
+
t_rec [definition, in
ABS.abs_defs]
+
t_ind [definition, in
ABS.abs_defs]
+
t_rect [definition, in
ABS.abs_defs]
+
t_int [constructor, in
ABS.abs_defs]
+
t_b [constructor, in
ABS.abs_defs]
+
T_sind [definition, in
ABS.abs_defs]
+
T_rec [definition, in
ABS.abs_defs]
+
T_ind [definition, in
ABS.abs_defs]
+
T_rect [definition, in
ABS.abs_defs]
+
T_int [constructor, in
ABS.abs_defs]
+
T_bool [constructor, in
ABS.abs_defs]
+
X
+
x [definition, in
ABS.abs_defs]
+
Z
+
z [definition, in
ABS.abs_defs]
+
+
Module Index
+
M
+
Map [in
ABS.abs_defs]
+
+
Variable Index
+
E
+
e_rect.H_list_e_cons [in
ABS.abs_defs]
+
e_rect.H_list_e_nil [in
ABS.abs_defs]
+
e_rect.H_e_fn_call [in
ABS.abs_defs]
+
e_rect.H_e_var [in
ABS.abs_defs]
+
e_rect.H_e_t [in
ABS.abs_defs]
+
e_rect.P_list_e [in
ABS.abs_defs]
+
e_rect.P_e [in
ABS.abs_defs]
+
+
Library Index
+
A
+
abs_functional_metatheory
+
abs_defs
+
+
Constructor Index
+
C
+
ctxv_sig [in
ABS.abs_defs]
+
ctxv_T [in
ABS.abs_defs]
+
E
+
e_fn_call [in
ABS.abs_defs]
+
e_var [in
ABS.abs_defs]
+
e_t [in
ABS.abs_defs]
+
F
+
F_fn [in
ABS.abs_defs]
+
R
+
red_fun_ground [in
ABS.abs_defs]
+
red_fun_exp [in
ABS.abs_defs]
+
red_var [in
ABS.abs_defs]
+
S
+
sig_sig [in
ABS.abs_defs]
+
T
+
typ_func_decl [in
ABS.abs_defs]
+
typ_func_expr [in
ABS.abs_defs]
+
typ_var [in
ABS.abs_defs]
+
typ_int [in
ABS.abs_defs]
+
typ_bool [in
ABS.abs_defs]
+
t_int [in
ABS.abs_defs]
+
t_b [in
ABS.abs_defs]
+
T_int [in
ABS.abs_defs]
+
T_bool [in
ABS.abs_defs]
+
+
Lemma Index
+
E
+
eq_z [in
ABS.abs_defs]
+
eq_b [in
ABS.abs_defs]
+
eq_x [in
ABS.abs_defs]
+
eq_fn [in
ABS.abs_defs]
+
eq_i [in
ABS.abs_defs]
+
T
+
type_preservation [in
ABS.abs_functional_metatheory]
+
+
Inductive Index
+
C
+
ctxv [in
ABS.abs_defs]
+
E
+
e [in
ABS.abs_defs]
+
F
+
F [in
ABS.abs_defs]
+
R
+
red_e [in
ABS.abs_defs]
+
S
+
sig [in
ABS.abs_defs]
+
T
+
t [in
ABS.abs_defs]
+
T [in
ABS.abs_defs]
+
typ_F [in
ABS.abs_defs]
+
typ_e [in
ABS.abs_defs]
+
+
Section Index
+
E
+
e_rect [in
ABS.abs_defs]
+
+
Definition Index
+
B
+
b [in
ABS.abs_defs]
+
C
+
ctxv_sind [in
ABS.abs_defs]
+
ctxv_rec [in
ABS.abs_defs]
+
ctxv_ind [in
ABS.abs_defs]
+
ctxv_rect [in
ABS.abs_defs]
+
E
+
e_ott_ind [in
ABS.abs_defs]
+
e_sind [in
ABS.abs_defs]
+
e_rec [in
ABS.abs_defs]
+
e_ind [in
ABS.abs_defs]
+
e_rect [in
ABS.abs_defs]
+
F
+
fn [in
ABS.abs_defs]
+
F_sind [in
ABS.abs_defs]
+
F_rec [in
ABS.abs_defs]
+
F_ind [in
ABS.abs_defs]
+
F_rect [in
ABS.abs_defs]
+
G
+
G [in
ABS.abs_defs]
+
G_vdash_s [in
ABS.abs_functional_metatheory]
+
I
+
i [in
ABS.abs_defs]
+
R
+
red_e_sind [in
ABS.abs_defs]
+
red_e_ind [in
ABS.abs_defs]
+
S
+
s [in
ABS.abs_defs]
+
sig_sind [in
ABS.abs_defs]
+
sig_rec [in
ABS.abs_defs]
+
sig_ind [in
ABS.abs_defs]
+
sig_rect [in
ABS.abs_defs]
+
subG [in
ABS.abs_functional_metatheory]
+
T
+
typ_F_sind [in
ABS.abs_defs]
+
typ_F_ind [in
ABS.abs_defs]
+
typ_e_sind [in
ABS.abs_defs]
+
typ_e_ind [in
ABS.abs_defs]
+
t_sind [in
ABS.abs_defs]
+
t_rec [in
ABS.abs_defs]
+
t_ind [in
ABS.abs_defs]
+
t_rect [in
ABS.abs_defs]
+
T_sind [in
ABS.abs_defs]
+
T_rec [in
ABS.abs_defs]
+
T_ind [in
ABS.abs_defs]
+
T_rect [in
ABS.abs_defs]
+
X
+
x [in
ABS.abs_defs]
+
Z
+
z [in
ABS.abs_defs]
+
+
+| Global Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(85 entries) |
+
+
+| Module Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(1 entry) |
+
+
+| Variable Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(7 entries) |
+
+
+| Library Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(2 entries) |
+
+
+| Constructor Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(19 entries) |
+
+
+| Lemma Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(6 entries) |
+
+
+| Inductive Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(9 entries) |
+
+
+| Section Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(1 entry) |
+
+
+| Definition Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(40 entries) |
+
+
+
+
+
About
+Welcome to the ABS Metatheory project website!
+Formal metatheory in Coq for the ABS language.
+Documentation
+
+
+
+
+