From 18a8299c25de2a94e70f328e650465276fed409b Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 13 Mar 2025 13:52:42 -0500
Subject: [PATCH 01/31] Add draft of desugaring

---
 user_manual.md | 348 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 348 insertions(+)

diff --git a/user_manual.md b/user_manual.md
index dcce018b..e657478f 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2164,3 +2164,351 @@ can be seen as syntax sugar for:
 
 If no conlusion is provided, then the type attribute is not specified.
 Notice this is only the case if the declaration of `r` does not involve `:assumption` or `:premise-list`.
+
+
+### Formal Definition of Preprocessor
+
+# Core syntax of terms
+
+```
+  <lit-category>  := '<numeral>' | '<decimal>' | '<rational>' | '<binary>' | '<hexadecimal>' | '<string>'
+  <attr>          :=  right-assoc-nil | right-assoc | left-assoc | left-assoc-nil |
+                      chainable | pairwise | binder | let-binder |
+                      program | oracle |
+                      list | opaque |
+                      datatype | datatype-constructor | amb-datatype-constructor |
+                      premise-list | none
+  <annot>         := [ <attr>, <pterm> ]
+  <term>          := <param> | <const> | (eo::var <term> <term>) |
+                      (-> <term> <term>) | (~> <term> <term>) | (eo::arrow <term>* <term>) |
+                      (_ <term> <term>) | (_# <term> <term>) | (<prog-const> <term>*)
+  <prog-const>    := <const> | eo::requires | eo::list_concat | eo::nil | eo::ite | eo::typeof | eo::is_eq
+
+  <pterm> := <term> | Null | (Opaque <pterm>) | (Quote <pterm>) | (Nil <pterm>*) | (Tuple <pterm>*) | (Lambda (Tuple <pterm>*) <pterm>) | Fail
+```
+
+# Parser State
+
+```
+  ; Symbol table.
+  S : maps strings to a list of <term>.
+  ; Attribute mapping.
+  A : maps <const> to <annot>.
+  ; Assertions (formulas provided in assert commands).
+  Ax : a list of <term>.
+  ; Category types, maps literal categories to their types.
+  L : maps <lit-category> to <term>
+```
+All state initially empty.
+
+
+# Desugaring of terms
+
+Takes as input the syntax given for a term. Returns a <pterm>.
+```
+DESUGAR(t):
+
+  ;;; annotations
+
+  (! T :implicit a_1 ... a_n):
+    return DESUGAR( (! Null a_1 ... a_n) )
+
+  (! T :opaque a_1 ... a_n), where T != Null:
+    return DESUGAR( (! (Opaque T) a_1 ... a_n) )
+
+  (! T :requires (t1 t2) a_1 ... a_n), where T != Null:
+    return DESUGAR( (! (eo::requires t_1 t_2 T) a_1 ... a_n) )
+
+  (! T :var x a_2 ... a_n), where T != Null, (Quote T_0) for any T_0:
+    Let x is a fresh parameter of type T.
+    return DESUGAR( (! (Quote x) a_2 ... a_n) )
+
+  (! t):
+    return DESUGAR(t)
+
+  ;;; function types
+
+  (-> Null T_1 ... T_n):
+    return DESUGAR( (-> T_1 ... T_n) )
+
+  (-> (Opaque T_0) ... (Opaque T_m) T_{m+1} ... T_n):
+    return (-> DESUGAR( (Opaque (Tuple T_0 ... T_m)) ) DESUGAR( (-> T_{m+1} ... T_n) ) )
+
+  (-> (eo::requires s1 s2 T_0) T_1 ... T_n):
+    return DESUGAR( (-> T_0 (eo::requires s1 s2 (-> T_1 ... T_n))) )
+
+  (-> (Quote T_0) ... T_n):
+    return (~> DESUGAR(T_0) DESUGAR( (-> T_1 ... T_n) ) )
+
+  (-> T_0 ... T_n), where n>0:
+    return (-> DESUGAR(T_0) DESUGAR( (-> T_1 ... T_n) ) )
+
+  (-> T_0):
+    return DESUGAR( T_0 )
+
+  ;;; binders, definitions
+
+  (f ((x_0 U_0) ... (x_m U_m)) t_1 ... t_n), where A(f) = [binder, c]:
+    Let [v_0, ..., v_m] = [(eo::var NAME(x_0) U_0) ... (eo::var NAME(x_m) U_m)]
+    return DESUGAR( SUBS( (f (c x_0 ... x_m) t_1 ... t_n), [x_0, ..., x_m], [v_0, ..., v_m]) )
+
+  (f ((x_0 s_0) ... (x_m s_m)) t), where A(f) = [let-binder, (Tuple lp lc)]:
+    Let [v_1, ..., v_m] = [(eo::var NAME(x_1) U_1) ... (eo::var NAME(x_m) U_m)]
+    return DESUGAR( SUBS( (f (lc (lp x_1 s_1) ... (lp x_m s_m)) t), [x_1, ..., x_m], [v_1, ..., v_m]) )
+
+  (f t_1 ... t_n), where A(f) = [define, (Lambda (Tuple x_1 ... x_n) t)]:
+    return DESUGAR( SUBS( t, [x_1, ..., x_n], [t_1, ..., t_n]) )
+
+  (eo::define ((x_1 s_1) ... (x_m s_m)) t):
+    return DESUGAR( SUBS( t, [x_1, ..., x_m], [s_1, ..., s_m]) )
+
+  ;;; match
+
+  (eo::match ((x_1 U_1) ... (x_m U_m)) t (((p_1 r_1) ... (p_n r_n)))):
+    Let [y_1, ..., y_k] = FREE_PARAMS(r_1, ..., r_n) \ [x_1, ..., x_m], having type [T_1, ..., T_k]
+    Let W, V be fresh parameters of type Type.
+    Let h = RUN( (program s ((x_1 U_1) ... (x_m U_m) (y_1 T_1) ... (y_k T_k))
+                    (W T_1 ... T_k) V
+                    ((((s p_1 y_1 ... y_k) r_1)
+                      ...
+                      ((s p_n y_1 ... y_k) r_n)))) )
+    return DESUGAR( (h t y_1 ... y_k) )
+
+  ;;; special operators
+
+  (_ t_1 ... t_n):
+    return DESUGAR( (t_1 ... t_n) )
+
+  (as f T), where A(f) = [amb-datatype-constructor, s]:
+    return (_# f DESUGAR(T) )
+
+  (eo::as f (-> T_1 ... T_n T)), where S[NAME(f)] = [f_1, ..., f_m]:
+    Let [k_1, ..., k_n] be fresh constants of type [T_1, ..., T_n]
+    return DESUGAR(
+      (eo::ite (eo::is_eq (eo::typeof (f_m k_1 ... k_n)) T) f_m
+      ...
+      (eo::ite (eo::is_eq (eo::typeof (f_1 k_1 ... k_n)) T) f_1
+                                                            Fail)...) )
+
+  ;;; pre-term operators
+
+  (Opaque t_1):
+    return (Opaque DESUGAR(t_1))
+
+  (Quote t_1):
+    return (Quote DESUGAR(t_1))
+
+  (Nil f t_1 ... t_n):
+    return (eo::nil f DESUGAR(t_1) ... DESUGAR(t_n))
+
+  ;;; n-ary kinds
+
+  ; where A(f) = [right-assoc-nil, c]:
+
+  (f t_1 ... t_n), where t_n != (Nil ...), A[t_n] != [list, Null]:
+    return DESUGAR( (f t_1 ... t_n (Nil f t_1 ... t_n)) )
+
+  (f t_1 ... t_n), where A[t_1] = [list, Null], n>1:
+    return (eo::list_concat f DESUGAR(t_1) DESUGAR( (f t_2 ... t_n) ))
+
+  (f t_1 ... t_n), where A[t_1] != [list, Null], n>1:
+    return (_ (_ f DESUGAR(t_1)) DESUGAR( (f t_2 ... t_n) ))
+
+  (f t_1), where A(f) = [right-assoc-nil, c]:
+    return DESUGAR(t_1)
+
+  ; where A(f) = [right-assoc, Null]:
+
+  (f t_1 ... t_n), where, n>1:
+    return (_ (_ f DESUGAR(t_1)) DESUGAR( (f t_2 ... t_n) ) )
+
+  (f t_1):
+    return DESUGAR(t_1)
+
+  ; where A(f) = [left-assoc-nil, c]:
+
+  (f t_1 ... t_n), where t_1 != (Nil ...), A[t_1] != [list, Null]:
+    return DESUGAR( (f (Nil f t_1 ... t_n) t_1 ... t_n) )
+
+  (f t_1 ... t_n), where A[t_1] = [list, Null], n>1:
+    return (eo::list_concat f DESUGAR( (f t_2 ... t_n) ) DESUGAR(t_1))
+
+  (f t_1 ... t_n), where A[t_1] != [list, Null], n>1:
+    return (_ (_ f DESUGAR( (f t_2 ... t_n) )) DESUGAR(t_1))
+
+  (f t_1):
+    return DESUGAR(t_1)
+
+  ; where A(f) = [left-assoc, Null]:
+
+  (f t_1 ... t_n), n>1:
+    return (_ (_ f DESUGAR( (f t_2 ... t_n) )) DESUGAR(t_1))
+
+  (f t_1):
+    return DESUGAR(t_1)
+
+  ; where A(f) = [chainable, c]:
+
+  (f t_1 t_2):
+    return (_ (_ f DESUGAR(t_1)) DESUGAR(t_2))
+
+  (f t_1 ... t_n), n != 2:
+    return DESUGAR( (c (f t_1 t_2) (f t_2 t_3) ... (f t_{n-1} t_n)) )
+
+  ; where A(f) = [pairwise, c]:
+
+  (f t_1 t_2):
+    return (_ (_ f DESUGAR(t_1)) DESUGAR(t_2))
+
+  (f t_1 ... t_n), n != 2:
+    return DESUGAR( (c (f t_1 t_2) (f t_1 t_3) ... (f t_2 t_3) ... (f t_{n-1} t_n)) )
+
+  ;;; opaque
+
+  ; where A(f) = [opaque, (Tuple T_1 ... T_m)]:
+
+  (f t_1 ... t_n), n = m:
+    return (_# (_# f DESUGAR(t_1)) ... DESUGAR(t_m))
+
+  (f t_1 ... t_n), n > m:
+    return DESUGAR( ((_# (_# f DESUGAR(t_1)) ... DESUGAR(t_m)) t_{m+1} ... t_n) )
+
+
+  ;;; programs, oracles, ordinary functions
+
+  (f t_1 ... t_n), where A(f) = [program, p]:
+    return (f DESUGAR(t_1) ... DESUGAR(t_n))
+
+  (f t_1 ... t_n), where A(f) = [oracle, s]:
+    return (f DESUGAR(t_1) ... DESUGAR(t_n))
+
+  (f t_1 ... t_n), n>1:
+    return (_ DESUGAR( (f t_1 ... t_{n-1}) ) t_n)
+
+  (f t_1):
+    return (_ f DESUGAR(t_1))
+
+  ;;; base case
+
+  s:
+    return s
+```
+
+
+# Desugaring of commands
+
+```
+(declare-const s T a), where the attribute of a is one of {right-assoc, right-assoc-nil, left-assoc, left-assoc-nil, pairwise, chainable, binder, let-binder, opaque, none}:
+  Let x = FRESH_CONST(s, DESUGAR(T))
+  A[x] := a
+  S[s] += x
+  return x
+
+(declare-const s T):
+  Let U = DESUGAR( T )
+  if U is (-> (Opaque U_1) ... (-> (Opaque U_n) V) ... )
+    return RUN( (declare-const s (-> U_1 ... U_n V) :opaque (Tuple U_1 ... U_n)) )
+  else
+    return RUN( (declare-const s U :none) )
+
+(declare-rule s ((y_1 U_1) ... (y_n U_n))
+  :premises (p_1 ... p_k)
+  :args (t_1 ... t_l)
+  :requires ((s_1 r_1) ... (s_1 s_m))
+  :conclusion F):
+  RUN( (declare-const s (-> (Quote t_1) ... (Quote t_l) (Proof p_1) ... (Proof p_k) (! F :requires (s_1 r_1) ... :requires (s_1 s_m)))) )
+
+(declare-rule s ((y_1 U_1) ... (y_n U_n))
+  :premise-list x c
+  :args (t_1 ... t_l)
+  :requires ((s_1 r_1) ... (s_1 s_m))
+  :conclusion F):
+  x = RUN( (declare-const s (-> (Quote t_1) ... (Quote t_l) (Proof x) (! F :requires (s_1 r_1) ... :requires (s_1 s_m)))) )
+  A[x] := [premise-list, c]
+
+(declare-rule x ((y_1 U_1) ... (y_n U_n))
+  :assumption a
+  :args (t_1 ... t_l)
+  :requires ((s_1 r_1) ... (s_1 s_m))
+  :conclusion F)
+  RUN( (declare-const s (-> (Quote t_1) ... (Quote t_l) (Proof p_1) ... (Proof p_k) (Proof a) (! F :requires (s_1 r_1) ... :requires (s_1 s_m)))) )
+
+(declare-type s (U_1 ... U_n)):
+  RUN( (declare-const s (-> U_1 ... U_n Type)) )
+
+(define s ((y_1 U_1) ... (y_n U_n)) t):
+  A[x] := [define, (Lambda (Tuple y_1 ... y_n) t)]
+  S[s] += x
+
+(declare-datatype s () (par (U_1 ... U_n) ((c_1 (s_11 T_11) ... (s1m T_1m)) ... (c_n (s_n1 T_n1) ... (snm T_nm))))):
+  Let DC = RUN( (declare-type s (U_1 ... U_n)) )
+  Let D = DESUGAR( (DC U_1 ... U_n) ) if n>0, or DC otherwise.
+  for i = 1 ... n:
+    for j = 1 ... m:
+      Let ds_ij = RUN( (declare-const s_ij (-> D T_ij)) )
+    Let sels = (Tuple ds_i1 ... ds_im).
+    if [U_1 ... U_n] is not a subset of FREE_PARAMS(T_i1, ..., T_im)
+      Let dc_i = RUN( (declare-const c_i (-> (Quote D) T_i1 ... T_im D)) )
+      A[dc_i] := [amb-datatype-constructor, sels]
+    else
+      Let dc_i = RUN( (declare-const c_i (-> T_i1 ... T_im D)) )
+      A[dc_i] := [amb-datatype-constructor, sels]
+  A[D] := [datatype, (Tuple dc_1 ... dc_n)]
+
+(declare-datatype s () ((c_1 (s_11 T_11) ... (s1m T_1m)) ... (c_n (s_n1 T_n1) ... (snm T_nm))))
+  RUN( (declare-datatype s () (par () ((c_1 (s_11 T_11) ... (s1m T_1m)) ... (c_n (s_n1 T_n1) ... (snm T_nm))))) )
+
+(assume s F):
+  ASSERT( F in Ax )
+  RUN( (declare-const s (Proof F)) )
+
+(step s F :rule r :premises (p_1 ... p_k) :args (t_1 ... t_n))
+  if A[r] = [premise-list, c]
+    RUN( (define s () (r t_1 ... t_n (ProofFromList c p_1 ... p_k))) )
+  else
+    RUN( (define s () (r t_1 ... t_n p_1 ... p_k)) )
+
+(program s ((x_1 U_1) ... (x_m U_m))
+  (T_1 ... T_n) T
+  (
+  ((s a_11 ... a_1n) r_0)
+  ...
+  ((s a_k1 ... y_kn) r_k)
+  )
+):
+  Let x = FRESH_CONST(s, DESUGAR((-> T_1 ... T_n T)))
+  A[x] := [program, (((s a_11 ... a_1n) r_0) ... ((s a_k1 ... y_kn) r_k))]
+  S[s] += x
+  return x
+
+;;; push/pop
+
+(assume-push s F)
+  RUN( (declare-const s (Proof F)) )
+
+
+(step-pop s F :rule r :premises (p_1 ... p_k) :args (t_1 ... t_n)), where (assume-push s G) is the assumption that is being popped:
+  TODO
+
+;;; SMT-LIB
+
+(declare-fun s () T):
+  RUN( (declare-const x T) )
+
+(declare-fun s (T_1 ... T_n) T):
+  RUN( (declare-const x (-> T_1 ... T_n T)) )
+
+(define-fun x ((y_1 U_1) ... (y_n U_n)) T t):
+  Ax := Ax ++ [DESUGAR( (= x (lambda ((y_1 U_1) ... (y_n U_n)) t)) )]
+  RUN( (declare-const x (-> U_1 ... U_n T)) )
+
+(define-fun x () T t):
+  Ax := Ax ++ [DESUGAR( (= x t) )]
+  RUN( (declare-const x T) )
+
+(assert F):
+  Ax := Ax ++ [F]
+
+(check-sat):
+  ; do nothing
+```

From df52ade1fd24638a0538c3d881b4b91049fb6312 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 13 Mar 2025 14:03:07 -0500
Subject: [PATCH 02/31] More

---
 user_manual.md | 222 +++++++++++++++++++++++++++----------------------
 1 file changed, 123 insertions(+), 99 deletions(-)

diff --git a/user_manual.md b/user_manual.md
index e657478f..1ef9d1e1 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2205,6 +2205,7 @@ All state initially empty.
 # Desugaring of terms
 
 Takes as input the syntax given for a term. Returns a <pterm>.
+
 ```
 DESUGAR(t):
 
@@ -2397,118 +2398,141 @@ DESUGAR(t):
 
 # Desugaring of commands
 
-```
-(declare-const s T a), where the attribute of a is one of {right-assoc, right-assoc-nil, left-assoc, left-assoc-nil, pairwise, chainable, binder, let-binder, opaque, none}:
-  Let x = FRESH_CONST(s, DESUGAR(T))
-  A[x] := a
-  S[s] += x
-  return x
-
-(declare-const s T):
-  Let U = DESUGAR( T )
-  if U is (-> (Opaque U_1) ... (-> (Opaque U_n) V) ... )
-    return RUN( (declare-const s (-> U_1 ... U_n V) :opaque (Tuple U_1 ... U_n)) )
-  else
-    return RUN( (declare-const s U :none) )
-
-(declare-rule s ((y_1 U_1) ... (y_n U_n))
-  :premises (p_1 ... p_k)
-  :args (t_1 ... t_l)
-  :requires ((s_1 r_1) ... (s_1 s_m))
-  :conclusion F):
-  RUN( (declare-const s (-> (Quote t_1) ... (Quote t_l) (Proof p_1) ... (Proof p_k) (! F :requires (s_1 r_1) ... :requires (s_1 s_m)))) )
-
-(declare-rule s ((y_1 U_1) ... (y_n U_n))
-  :premise-list x c
-  :args (t_1 ... t_l)
-  :requires ((s_1 r_1) ... (s_1 s_m))
-  :conclusion F):
-  x = RUN( (declare-const s (-> (Quote t_1) ... (Quote t_l) (Proof x) (! F :requires (s_1 r_1) ... :requires (s_1 s_m)))) )
-  A[x] := [premise-list, c]
-
-(declare-rule x ((y_1 U_1) ... (y_n U_n))
-  :assumption a
-  :args (t_1 ... t_l)
-  :requires ((s_1 r_1) ... (s_1 s_m))
-  :conclusion F)
-  RUN( (declare-const s (-> (Quote t_1) ... (Quote t_l) (Proof p_1) ... (Proof p_k) (Proof a) (! F :requires (s_1 r_1) ... :requires (s_1 s_m)))) )
-
-(declare-type s (U_1 ... U_n)):
-  RUN( (declare-const s (-> U_1 ... U_n Type)) )
-
-(define s ((y_1 U_1) ... (y_n U_n)) t):
-  A[x] := [define, (Lambda (Tuple y_1 ... y_n) t)]
-  S[s] += x
-
-(declare-datatype s () (par (U_1 ... U_n) ((c_1 (s_11 T_11) ... (s1m T_1m)) ... (c_n (s_n1 T_n1) ... (snm T_nm))))):
-  Let DC = RUN( (declare-type s (U_1 ... U_n)) )
-  Let D = DESUGAR( (DC U_1 ... U_n) ) if n>0, or DC otherwise.
-  for i = 1 ... n:
-    for j = 1 ... m:
-      Let ds_ij = RUN( (declare-const s_ij (-> D T_ij)) )
-    Let sels = (Tuple ds_i1 ... ds_im).
-    if [U_1 ... U_n] is not a subset of FREE_PARAMS(T_i1, ..., T_im)
-      Let dc_i = RUN( (declare-const c_i (-> (Quote D) T_i1 ... T_im D)) )
-      A[dc_i] := [amb-datatype-constructor, sels]
-    else
-      Let dc_i = RUN( (declare-const c_i (-> T_i1 ... T_im D)) )
-      A[dc_i] := [amb-datatype-constructor, sels]
-  A[D] := [datatype, (Tuple dc_1 ... dc_n)]
+Takes as input the syntax given for a command. Optionally returns a <const>.
 
-(declare-datatype s () ((c_1 (s_11 T_11) ... (s1m T_1m)) ... (c_n (s_n1 T_n1) ... (snm T_nm))))
-  RUN( (declare-datatype s () (par () ((c_1 (s_11 T_11) ... (s1m T_1m)) ... (c_n (s_n1 T_n1) ... (snm T_nm))))) )
+```
+RUN(C):
 
-(assume s F):
-  ASSERT( F in Ax )
-  RUN( (declare-const s (Proof F)) )
+  (declare-const s T a), where the attribute of a is one of 
+  {right-assoc, right-assoc-nil, left-assoc, left-assoc-nil, pairwise, chainable, binder, let-binder, opaque, none}:
+    Let x = FRESH_CONST(s, DESUGAR(T))
+    A[x] := a
+    S[s] += x
+    return x
 
-(step s F :rule r :premises (p_1 ... p_k) :args (t_1 ... t_n))
-  if A[r] = [premise-list, c]
-    RUN( (define s () (r t_1 ... t_n (ProofFromList c p_1 ... p_k))) )
-  else
-    RUN( (define s () (r t_1 ... t_n p_1 ... p_k)) )
+  (declare-const s T):
+    Let U = DESUGAR( T )
+    if U is (-> (Opaque U_1) ... (-> (Opaque U_n) V) ... )
+      return RUN( (declare-const s (-> U_1 ... U_n V) :opaque (Tuple U_1 ... U_n)) )
+    else
+      return RUN( (declare-const s U :none) )
+
+  (declare-rule s ((y_1 U_1) ... (y_n U_n))
+    :premises (p_1 ... p_k)
+    :args (t_1 ... t_l)
+    :requires ((s_1 r_1) ... (s_1 s_m))
+    :conclusion F):
+    return RUN( 
+      (declare-const s (-> (Quote t_1) ... (Quote t_l) 
+                          (Proof p_1) ... (Proof p_k) 
+                          (! F :requires (s_1 r_1) ... :requires (s_1 s_m)))) )
+
+  (declare-rule s ((y_1 U_1) ... (y_n U_n))
+    :premise-list x c
+    :args (t_1 ... t_l)
+    :requires ((s_1 r_1) ... (s_1 s_m))
+    :conclusion F):
+    x = RUN( 
+      (declare-const s (-> (Quote t_1) ... (Quote t_l) 
+                          (Proof x)
+                          (! F :requires (s_1 r_1) ... :requires (s_1 s_m)))) )
+    A[x] := [premise-list, c]
+    return x
+
+  (declare-rule x ((y_1 U_1) ... (y_n U_n))
+    :assumption a
+    :args (t_1 ... t_l)
+    :requires ((s_1 r_1) ... (s_1 s_m))
+    :conclusion F):
+    return RUN( 
+      (declare-const s (-> (Quote t_1) ... (Quote t_l) 
+                          (Proof p_1) ... (Proof p_k) (Proof a) 
+                          (! F :requires (s_1 r_1) ... :requires (s_1 s_m)))) )
+
+  (declare-type s (U_1 ... U_n)):
+    return RUN( (declare-const s (-> U_1 ... U_n Type)) )
+
+  (define s ((y_1 U_1) ... (y_n U_n)) t):
+    A[x] := [define, (Lambda (Tuple y_1 ... y_n) t)]
+    S[s] += x
+    return x
+
+  (declare-datatype s () (par (U_1 ... U_n) ((c_1 (s_11 T_11) ... (s1m T_1m)) ... (c_n (s_n1 T_n1) ... (snm T_nm))))):
+    Let DC = RUN( (declare-type s (U_1 ... U_n)) )
+    Let D = DESUGAR( (DC U_1 ... U_n) ) if n>0, or DC otherwise.
+    for i = 1 ... n:
+      for j = 1 ... m:
+        Let ds_ij = RUN( (declare-const s_ij (-> D T_ij)) )
+      Let sels = (Tuple ds_i1 ... ds_im).
+      if [U_1 ... U_n] is not a subset of FREE_PARAMS(T_i1, ..., T_im)
+        Let dc_i = RUN( (declare-const c_i (-> (Quote D) T_i1 ... T_im D)) )
+        A[dc_i] := [amb-datatype-constructor, sels]
+      else
+        Let dc_i = RUN( (declare-const c_i (-> T_i1 ... T_im D)) )
+        A[dc_i] := [amb-datatype-constructor, sels]
+    A[DC] := [datatype, (Tuple dc_1 ... dc_n)]
+    return DC
+
+  (declare-datatype s () ((c_1 (s_11 T_11) ... (s1m T_1m)) ... (c_n (s_n1 T_n1) ... (snm T_nm)))):
+    return RUN( (declare-datatype s () (par () ((c_1 (s_11 T_11) ... (s1m T_1m)) ... (c_n (s_n1 T_n1) ... (snm T_nm))))) )
+
+  (assume s F):
+    ASSERT( F in Ax )
+    return RUN( (declare-const s (Proof F)) )
+
+  (step s F :rule r :premises (p_1 ... p_k) :args (t_1 ... t_n)):
+    if A[r] = [premise-list, c]
+      return RUN( (define s () (r t_1 ... t_n (ProofFromList c p_1 ... p_k))) )
+    else
+      return RUN( (define s () (r t_1 ... t_n p_1 ... p_k)) )
 
-(program s ((x_1 U_1) ... (x_m U_m))
-  (T_1 ... T_n) T
-  (
-  ((s a_11 ... a_1n) r_0)
-  ...
-  ((s a_k1 ... y_kn) r_k)
-  )
-):
-  Let x = FRESH_CONST(s, DESUGAR((-> T_1 ... T_n T)))
-  A[x] := [program, (((s a_11 ... a_1n) r_0) ... ((s a_k1 ... y_kn) r_k))]
-  S[s] += x
-  return x
+  (program s ((x_1 U_1) ... (x_m U_m))
+    (T_1 ... T_n) T
+    (
+    ((s a_11 ... a_1n) r_0)
+    ...
+    ((s a_k1 ... y_kn) r_k)
+    )
+  ):
+    Let x = FRESH_CONST(s, DESUGAR((eo::arrow T_1 ... T_n T)))
+    A[x] := [program, (((s a_11 ... a_1n) r_0) ... ((s a_k1 ... y_kn) r_k))]
+    S[s] += x
+    return x
+  
+  (declare-oracle-fun s () T o):
+    return RUN( (declare-const s T :oracle o) )
 
-;;; push/pop
+  (declare-oracle-fun s (T_1 ... T_n) T o):
+    return RUN( (declare-const s (eo::arrow T_1 ... T_n T) :oracle o) )
 
-(assume-push s F)
-  RUN( (declare-const s (Proof F)) )
+  ;;; push/pop
 
+  (assume-push s F)
+    return RUN( (declare-const s (Proof F)) )
 
-(step-pop s F :rule r :premises (p_1 ... p_k) :args (t_1 ... t_n)), where (assume-push s G) is the assumption that is being popped:
-  TODO
+  (step-pop s F :rule r :premises (p_1 ... p_k) :args (t_1 ... t_n)), where (assume-push s G)
+  is the assumption that is being popped:
+    TODO
 
-;;; SMT-LIB
+  ;;; SMT-LIB
 
-(declare-fun s () T):
-  RUN( (declare-const x T) )
+  (declare-fun s () T):
+    RUN( (declare-const x T) )
 
-(declare-fun s (T_1 ... T_n) T):
-  RUN( (declare-const x (-> T_1 ... T_n T)) )
+  (declare-fun s (T_1 ... T_n) T):
+    RUN( (declare-const x (-> T_1 ... T_n T)) )
 
-(define-fun x ((y_1 U_1) ... (y_n U_n)) T t):
-  Ax := Ax ++ [DESUGAR( (= x (lambda ((y_1 U_1) ... (y_n U_n)) t)) )]
-  RUN( (declare-const x (-> U_1 ... U_n T)) )
+  (define-fun x () T t):
+    Ax := Ax ++ [DESUGAR( (= x t) )]  ; assumes user definition of =.
+    RUN( (declare-const x T) )
 
-(define-fun x () T t):
-  Ax := Ax ++ [DESUGAR( (= x t) )]
-  RUN( (declare-const x T) )
+  (define-fun x ((y_1 U_1) ... (y_n U_n)) T t):
+    Ax := Ax ++ [DESUGAR( (= x (lambda ((y_1 U_1) ... (y_n U_n)) t)) )] ; assumes user definition of =, lambda.
+    RUN( (declare-const x (-> U_1 ... U_n T)) )
 
-(assert F):
-  Ax := Ax ++ [F]
+  (assert F):
+    Ax := Ax ++ [F]
 
-(check-sat):
-  ; do nothing
+  (check-sat):
+    ; do nothing
 ```

From e8b4932e2687607803f293eb7e465b11c17a12d9 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 13 Mar 2025 14:04:28 -0500
Subject: [PATCH 03/31] More

---
 user_manual.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/user_manual.md b/user_manual.md
index 1ef9d1e1..e17eaec1 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2180,7 +2180,7 @@ Notice this is only the case if the declaration of `r` does not involve `:assump
                       premise-list | none
   <annot>         := [ <attr>, <pterm> ]
   <term>          := <param> | <const> | (eo::var <term> <term>) |
-                      (-> <term> <term>) | (~> <term> <term>) | (eo::arrow <term>* <term>) |
+                      (-> <term> <term>) | (~> <term> <term>) | (--> <term>* <term>) |
                       (_ <term> <term>) | (_# <term> <term>) | (<prog-const> <term>*)
   <prog-const>    := <const> | eo::requires | eo::list_concat | eo::nil | eo::ite | eo::typeof | eo::is_eq
 
@@ -2494,7 +2494,7 @@ RUN(C):
     ((s a_k1 ... y_kn) r_k)
     )
   ):
-    Let x = FRESH_CONST(s, DESUGAR((eo::arrow T_1 ... T_n T)))
+    Let x = FRESH_CONST(s, DESUGAR((--> T_1 ... T_n T)))
     A[x] := [program, (((s a_11 ... a_1n) r_0) ... ((s a_k1 ... y_kn) r_k))]
     S[s] += x
     return x
@@ -2503,7 +2503,7 @@ RUN(C):
     return RUN( (declare-const s T :oracle o) )
 
   (declare-oracle-fun s (T_1 ... T_n) T o):
-    return RUN( (declare-const s (eo::arrow T_1 ... T_n T) :oracle o) )
+    return RUN( (declare-const s (--> T_1 ... T_n T) :oracle o) )
 
   ;;; push/pop
 

From 2b5cc195f04cf7376833366527a8c7f804ef173f Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 13 Mar 2025 14:09:37 -0500
Subject: [PATCH 04/31] More

---
 user_manual.md | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/user_manual.md b/user_manual.md
index e17eaec1..df520419 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2505,6 +2505,9 @@ RUN(C):
   (declare-oracle-fun s (T_1 ... T_n) T o):
     return RUN( (declare-const s (--> T_1 ... T_n T) :oracle o) )
 
+  (declare-consts cat T)
+    L[cat] := T
+
   ;;; push/pop
 
   (assume-push s F)
@@ -2517,18 +2520,18 @@ RUN(C):
   ;;; SMT-LIB
 
   (declare-fun s () T):
-    RUN( (declare-const x T) )
+    return RUN( (declare-const x T) )
 
   (declare-fun s (T_1 ... T_n) T):
-    RUN( (declare-const x (-> T_1 ... T_n T)) )
+    return RUN( (declare-const x (-> T_1 ... T_n T)) )
 
   (define-fun x () T t):
     Ax := Ax ++ [DESUGAR( (= x t) )]  ; assumes user definition of =.
-    RUN( (declare-const x T) )
+    return RUN( (declare-const x T) )
 
   (define-fun x ((y_1 U_1) ... (y_n U_n)) T t):
     Ax := Ax ++ [DESUGAR( (= x (lambda ((y_1 U_1) ... (y_n U_n)) t)) )] ; assumes user definition of =, lambda.
-    RUN( (declare-const x (-> U_1 ... U_n T)) )
+    return RUN( (declare-const x (-> U_1 ... U_n T)) )
 
   (assert F):
     Ax := Ax ++ [F]

From 7a25c2cf24661d24445818edff95224607d115b4 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 13 Mar 2025 14:20:02 -0500
Subject: [PATCH 05/31] More

---
 user_manual.md | 36 +++++++++++++++++++-----------------
 1 file changed, 19 insertions(+), 17 deletions(-)

diff --git a/user_manual.md b/user_manual.md
index df520419..6eae624d 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2184,7 +2184,8 @@ Notice this is only the case if the declaration of `r` does not involve `:assump
                       (_ <term> <term>) | (_# <term> <term>) | (<prog-const> <term>*)
   <prog-const>    := <const> | eo::requires | eo::list_concat | eo::nil | eo::ite | eo::typeof | eo::is_eq
 
-  <pterm> := <term> | Null | (Opaque <pterm>) | (Quote <pterm>) | (Nil <pterm>*) | (Tuple <pterm>*) | (Lambda (Tuple <pterm>*) <pterm>) | Fail
+  <pterm>         := <term> | Null | (Opaque <pterm>) | (Quote <pterm>) | (Nil <pterm>*) |
+                     (Tuple <pterm>*) | (Lambda (Tuple <pterm>*) <pterm>) | Fail
 ```
 
 # Parser State
@@ -2403,8 +2404,7 @@ Takes as input the syntax given for a command. Optionally returns a <const>.
 ```
 RUN(C):
 
-  (declare-const s T a), where the attribute of a is one of 
-  {right-assoc, right-assoc-nil, left-assoc, left-assoc-nil, pairwise, chainable, binder, let-binder, opaque, none}:
+  (declare-const s T a):
     Let x = FRESH_CONST(s, DESUGAR(T))
     A[x] := a
     S[s] += x
@@ -2423,9 +2423,9 @@ RUN(C):
     :requires ((s_1 r_1) ... (s_1 s_m))
     :conclusion F):
     return RUN( 
-      (declare-const s (-> (Quote t_1) ... (Quote t_l) 
-                          (Proof p_1) ... (Proof p_k) 
-                          (! F :requires (s_1 r_1) ... :requires (s_1 s_m)))) )
+      (declare-const s (-> (Quote t_1) ... (Quote t_l)
+                           (Proof p_1) ... (Proof p_k)
+                           (! F :requires (s_1 r_1) ... :requires (s_1 s_m)))) )
 
   (declare-rule s ((y_1 U_1) ... (y_n U_n))
     :premise-list x c
@@ -2433,9 +2433,9 @@ RUN(C):
     :requires ((s_1 r_1) ... (s_1 s_m))
     :conclusion F):
     x = RUN( 
-      (declare-const s (-> (Quote t_1) ... (Quote t_l) 
-                          (Proof x)
-                          (! F :requires (s_1 r_1) ... :requires (s_1 s_m)))) )
+      (declare-const s (-> (Quote t_1) ... (Quote t_l)
+                           (Proof x)
+                           (! F :requires (s_1 r_1) ... :requires (s_1 s_m)))) )
     A[x] := [premise-list, c]
     return x
 
@@ -2445,9 +2445,9 @@ RUN(C):
     :requires ((s_1 r_1) ... (s_1 s_m))
     :conclusion F):
     return RUN( 
-      (declare-const s (-> (Quote t_1) ... (Quote t_l) 
-                          (Proof p_1) ... (Proof p_k) (Proof a) 
-                          (! F :requires (s_1 r_1) ... :requires (s_1 s_m)))) )
+      (declare-const s (-> (Quote t_1) ... (Quote t_l)
+                           (Proof p_1) ... (Proof p_k) (Proof a)
+                           (! F :requires (s_1 r_1) ... :requires (s_1 s_m)))) )
 
   (declare-type s (U_1 ... U_n)):
     return RUN( (declare-const s (-> U_1 ... U_n Type)) )
@@ -2474,7 +2474,11 @@ RUN(C):
     return DC
 
   (declare-datatype s () ((c_1 (s_11 T_11) ... (s1m T_1m)) ... (c_n (s_n1 T_n1) ... (snm T_nm)))):
-    return RUN( (declare-datatype s () (par () ((c_1 (s_11 T_11) ... (s1m T_1m)) ... (c_n (s_n1 T_n1) ... (snm T_nm))))) )
+    return RUN( (declare-datatype s ()
+                  (par () ((c_1 (s_11 T_11) ... (s1m T_1m)) ... (c_n (s_n1 T_n1) ... (snm T_nm))))) )
+
+  (declare-datatypes ...):
+    TODO
 
   (assume s F):
     ASSERT( F in Ax )
@@ -2494,10 +2498,8 @@ RUN(C):
     ((s a_k1 ... y_kn) r_k)
     )
   ):
-    Let x = FRESH_CONST(s, DESUGAR((--> T_1 ... T_n T)))
-    A[x] := [program, (((s a_11 ... a_1n) r_0) ... ((s a_k1 ... y_kn) r_k))]
-    S[s] += x
-    return x
+    return RUN( (declare-const s (--> T_1 ... T_n T)
+                  :program (Tuple (Tuple (f a_11 ... a_1n) r_0) ... (Tuple (f a_k1 ... y_kn) r_k))) )
   
   (declare-oracle-fun s () T o):
     return RUN( (declare-const s T :oracle o) )

From 5812a40ab76f5452f03dc88be82cb3053018d76f Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 13 Mar 2025 15:32:53 -0500
Subject: [PATCH 06/31] More

---
 user_manual.md | 120 ++++++++++++++++++++++++++++++++++---------------
 1 file changed, 85 insertions(+), 35 deletions(-)

diff --git a/user_manual.md b/user_manual.md
index 6eae624d..088fd969 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2035,13 +2035,14 @@ When streaming input to Ethos, we assume the input is being given for a proof fi
 ;;;
 <keyword>       ::= :<symbol>
 <attr>          ::= <keyword> <term>?
-<term>          ::= <symbol> | (<symbol> <term>+) | (! <term> <attr>+) | (eo::match (<typed-param>*) <term> ((<term> <term>)*))
+<term>          ::= <symbol> | (<symbol> <term>+) | (! <term> <attr>+) | (eo::match (<typed-param>*) <term> ((<term> <term>)*)) |
+                    (<symbol> (<typed-param>*) <term>*) | (<symbol> ((<symbol> <term>)*) <term>)
 <type>          ::= <term>
 <typed-param>   ::= (<symbol> <type> <attr>*)
 <sort-dec>      ::= (<symbol> <numeral>)
 <sel-dec>       ::= (<symbol> <type>)
 <cons-dec>      ::= (<symbol> <sel-dec>*)
-<datatype-dec>  ::= (<cons-dec>+)
+<datatype-dec>  ::= (<cons-dec>+) | (par (<symbol>+) (<cons-dec>+))
 <lit-category>  ::= '<numeral>' | '<decimal>' | '<rational>' | '<binary>' | '<hexadecimal>' | '<string>'
 
 ;;;
@@ -2166,9 +2167,21 @@ If no conlusion is provided, then the type attribute is not specified.
 Notice this is only the case if the declaration of `r` does not involve `:assumption` or `:premise-list`.
 
 
-### Formal Definition of Preprocessor
+# Formal Definition of Preprocessor
 
-# Core syntax of terms
+### Core syntax of terms
+
+The category <term> denotes all terms and types.
+This includes parameters, constants, and variables.
+In detail,
+`->` is function arrow, `~>` is quote arrow, `-->` is program arrow, 
+`_` is application and `_#` is opaque application.
+
+The category <pterm> denotes "pre-terms", which include intermediate constructors that are used in the desugar mentioned below.
+Constructors specific to pre-terms are not expected to be returned by the desugar method for a well-formed term.
+In particular, this means that annotations e.g. `:implicit`, `:opaque`, `:var` should not appear anywhere by in function arguments, symbols introduced by the command `define` must be fully applied.
+
+Pre-terms may appear as the second field of term annotations <annot>.
 
 ```
   <lit-category>  := '<numeral>' | '<decimal>' | '<rational>' | '<binary>' | '<hexadecimal>' | '<string>'
@@ -2182,13 +2195,13 @@ Notice this is only the case if the declaration of `r` does not involve `:assump
   <term>          := <param> | <const> | (eo::var <term> <term>) |
                       (-> <term> <term>) | (~> <term> <term>) | (--> <term>* <term>) |
                       (_ <term> <term>) | (_# <term> <term>) | (<prog-const> <term>*)
-  <prog-const>    := <const> | eo::requires | eo::list_concat | eo::nil | eo::ite | eo::typeof | eo::is_eq
+  <prog-const>    := <const> | eo::requires | eo::nil | eo::ite | eo::typeof | eo::is_eq
 
   <pterm>         := <term> | Null | (Opaque <pterm>) | (Quote <pterm>) | (Nil <pterm>*) |
-                     (Tuple <pterm>*) | (Lambda (Tuple <pterm>*) <pterm>) | Fail
+                     (Tuple <pterm>*) | (Lambda (Tuple <pterm>*) <pterm>)
 ```
 
-# Parser State
+### Parser State
 
 ```
   ; Symbol table.
@@ -2200,12 +2213,49 @@ Notice this is only the case if the declaration of `r` does not involve `:assump
   ; Category types, maps literal categories to their types.
   L : maps <lit-category> to <term>
 ```
-All state initially empty.
 
+The initial state can be understood by parsing the following background definitions:
+```
+(declare-const Bool Type)
+(declare-consts <boolean> Bool)
+
+; Definitions of applicaable eo::
+```
+
+### Scoping of parameters
+
+Parameter lists `(<typed-param>*)` introduce fresh parameters that are processed as follows.
+
+A typed parameter `(x T)` in a type parameter list constructs a fresh parameter term (independent of whether another parameter of that name and type already exist), and adds `x` to the symbol table `S` in the duration `x` is in scope. 
 
-# Desugaring of terms
+In particular,
+parameters introduced by a list at the beginning of commands
+`define`, `declare-parameterized-const`, `program`, `define-fun`, `declare-rule`
+are in scope for the remainder of the command.
+Parameters introduced at the term level e.g. by `eo::match`, `eo::define`, or as the first argument of functions having attribute `binder` or `let-binder` are in the scope only in further arguments to that term.
+As an exception,
+parameters marked `(x T :implicit)` are only in scope in the remainder of parsing the parameter list, 
+and are omitted from the parameter list after they are parsed.
+
+Parameters are generated in several other special contexts.
+In parameteric datatype definitions `(par (U_1 ... U_n) (<cons-dec>+))`, 
+`U_1, ..., U_n` are fresh parameters of type `Type` that are in scope of the definition of the constructors for that datatype.
+In variable annotations, e.g. `(-> (! T :var x) U)`, 
+`x` is a fresh parameter of type `T`, and is in scope of the remainder of the arguments to the function type.
+
+Parameters marked with the annotation `(x T :list)` are such that the attribute map `A(x)` is set to `[list, Null]`.
+
+### Desugaring of terms
 
 Takes as input the syntax given for a term. Returns a <pterm>.
+We use meta-variables `t_i, s_j` to denote terms, `T_i, U_j, V_k` to denote types (terms whose type is Type), `a_i, a_j` to denote annotations.
+We use `f` to denote a term of some function type.
+
+We assume the following helper methods:
+- `NAME(x)`: returns a string corresponding to the name of parameter or constant x.
+- `FREE_PARAMS(t)`: returns the set of parameters that occur as subterms of t.
+- `SUBS( t, [x_1, ..., x_n], [s_1, ..., s_n] )`: returns the result of replacing all occurrences of parameters `x_1, ..., x_n` by `s_1, ..., s_n` simultaneously.
+
 
 ```
 DESUGAR(t):
@@ -2221,9 +2271,9 @@ DESUGAR(t):
   (! T :requires (t1 t2) a_1 ... a_n), where T != Null:
     return DESUGAR( (! (eo::requires t_1 t_2 T) a_1 ... a_n) )
 
-  (! T :var x a_2 ... a_n), where T != Null, (Quote T_0) for any T_0:
+  (! T :var x a_1 ... a_n), where T != Null, (Quote U) for any U:
     Let x is a fresh parameter of type T.
-    return DESUGAR( (! (Quote x) a_2 ... a_n) )
+    return DESUGAR( (! (Quote x) a_1 ... a_n) )
 
   (! t):
     return DESUGAR(t)
@@ -2233,9 +2283,6 @@ DESUGAR(t):
   (-> Null T_1 ... T_n):
     return DESUGAR( (-> T_1 ... T_n) )
 
-  (-> (Opaque T_0) ... (Opaque T_m) T_{m+1} ... T_n):
-    return (-> DESUGAR( (Opaque (Tuple T_0 ... T_m)) ) DESUGAR( (-> T_{m+1} ... T_n) ) )
-
   (-> (eo::requires s1 s2 T_0) T_1 ... T_n):
     return DESUGAR( (-> T_0 (eo::requires s1 s2 (-> T_1 ... T_n))) )
 
@@ -2250,13 +2297,13 @@ DESUGAR(t):
 
   ;;; binders, definitions
 
-  (f ((x_0 U_0) ... (x_m U_m)) t_1 ... t_n), where A(f) = [binder, c]:
-    Let [v_0, ..., v_m] = [(eo::var NAME(x_0) U_0) ... (eo::var NAME(x_m) U_m)]
-    return DESUGAR( SUBS( (f (c x_0 ... x_m) t_1 ... t_n), [x_0, ..., x_m], [v_0, ..., v_m]) )
+  (f ((x_1 U_1) ... (x_m U_m)) t_1 ... t_n), where A(f) = [binder, g]:
+    Let [v_1, ..., v_m] = [(eo::var NAME(x_1) U_1) ... (eo::var NAME(x_m) U_m)]
+    return DESUGAR( SUBS( (f (g x_1 ... x_m) t_1 ... t_n), [x_1, ..., x_m], [v_1, ..., v_m]) )
 
-  (f ((x_0 s_0) ... (x_m s_m)) t), where A(f) = [let-binder, (Tuple lp lc)]:
+  (f ((x_1 s_1) ... (x_m s_m)) t), where A(f) = [let-binder, (Tuple lp ll)]:
     Let [v_1, ..., v_m] = [(eo::var NAME(x_1) U_1) ... (eo::var NAME(x_m) U_m)]
-    return DESUGAR( SUBS( (f (lc (lp x_1 s_1) ... (lp x_m s_m)) t), [x_1, ..., x_m], [v_1, ..., v_m]) )
+    return DESUGAR( SUBS( (f (ll (lp x_1 s_1) ... (lp x_m s_m)) t), [x_1, ..., x_m], [v_1, ..., v_m]) )
 
   (f t_1 ... t_n), where A(f) = [define, (Lambda (Tuple x_1 ... x_n) t)]:
     return DESUGAR( SUBS( t, [x_1, ..., x_n], [t_1, ..., t_n]) )
@@ -2289,8 +2336,8 @@ DESUGAR(t):
     return DESUGAR(
       (eo::ite (eo::is_eq (eo::typeof (f_m k_1 ... k_n)) T) f_m
       ...
-      (eo::ite (eo::is_eq (eo::typeof (f_1 k_1 ... k_n)) T) f_1
-                                                            Fail)...) )
+      (eo::ite (eo::is_eq (eo::typeof (f_2 k_1 ... k_n)) T) f_2
+        (eo::requires (eo::typeof (f_1 k_1 ... k_n)) T f_1)...)) )
 
   ;;; pre-term operators
 
@@ -2305,7 +2352,7 @@ DESUGAR(t):
 
   ;;; n-ary kinds
 
-  ; where A(f) = [right-assoc-nil, c]:
+  ; where A(f) = [right-assoc-nil, g]:
 
   (f t_1 ... t_n), where t_n != (Nil ...), A[t_n] != [list, Null]:
     return DESUGAR( (f t_1 ... t_n (Nil f t_1 ... t_n)) )
@@ -2316,7 +2363,7 @@ DESUGAR(t):
   (f t_1 ... t_n), where A[t_1] != [list, Null], n>1:
     return (_ (_ f DESUGAR(t_1)) DESUGAR( (f t_2 ... t_n) ))
 
-  (f t_1), where A(f) = [right-assoc-nil, c]:
+  (f t_1), where A(f) = [right-assoc-nil, g]:
     return DESUGAR(t_1)
 
   ; where A(f) = [right-assoc, Null]:
@@ -2327,7 +2374,7 @@ DESUGAR(t):
   (f t_1):
     return DESUGAR(t_1)
 
-  ; where A(f) = [left-assoc-nil, c]:
+  ; where A(f) = [left-assoc-nil, g]:
 
   (f t_1 ... t_n), where t_1 != (Nil ...), A[t_1] != [list, Null]:
     return DESUGAR( (f (Nil f t_1 ... t_n) t_1 ... t_n) )
@@ -2349,21 +2396,21 @@ DESUGAR(t):
   (f t_1):
     return DESUGAR(t_1)
 
-  ; where A(f) = [chainable, c]:
+  ; where A(f) = [chainable, g]:
 
   (f t_1 t_2):
     return (_ (_ f DESUGAR(t_1)) DESUGAR(t_2))
 
   (f t_1 ... t_n), n != 2:
-    return DESUGAR( (c (f t_1 t_2) (f t_2 t_3) ... (f t_{n-1} t_n)) )
+    return DESUGAR( (g (f t_1 t_2) (f t_2 t_3) ... (f t_{n-1} t_n)) )
 
-  ; where A(f) = [pairwise, c]:
+  ; where A(f) = [pairwise, g]:
 
   (f t_1 t_2):
     return (_ (_ f DESUGAR(t_1)) DESUGAR(t_2))
 
   (f t_1 ... t_n), n != 2:
-    return DESUGAR( (c (f t_1 t_2) (f t_1 t_3) ... (f t_2 t_3) ... (f t_{n-1} t_n)) )
+    return DESUGAR( (g (f t_1 t_2) (f t_1 t_3) ... (f t_2 t_3) ... (f t_{n-1} t_n)) )
 
   ;;; opaque
 
@@ -2392,8 +2439,8 @@ DESUGAR(t):
 
   ;;; base case
 
-  s:
-    return s
+  t:
+    return t
 ```
 
 
@@ -2411,12 +2458,15 @@ RUN(C):
     return x
 
   (declare-const s T):
-    Let U = DESUGAR( T )
+    Let U = DESUGAR(T)
     if U is (-> (Opaque U_1) ... (-> (Opaque U_n) V) ... )
       return RUN( (declare-const s (-> U_1 ... U_n V) :opaque (Tuple U_1 ... U_n)) )
     else
       return RUN( (declare-const s U :none) )
 
+  (declare-parameterized-const ((y_1 U_1) ... (y_n U_n)) T a):
+    TODO
+
   (declare-rule s ((y_1 U_1) ... (y_n U_n))
     :premises (p_1 ... p_k)
     :args (t_1 ... t_l)
@@ -2428,7 +2478,7 @@ RUN(C):
                            (! F :requires (s_1 r_1) ... :requires (s_1 s_m)))) )
 
   (declare-rule s ((y_1 U_1) ... (y_n U_n))
-    :premise-list x c
+    :premise-list x g
     :args (t_1 ... t_l)
     :requires ((s_1 r_1) ... (s_1 s_m))
     :conclusion F):
@@ -2436,7 +2486,7 @@ RUN(C):
       (declare-const s (-> (Quote t_1) ... (Quote t_l)
                            (Proof x)
                            (! F :requires (s_1 r_1) ... :requires (s_1 s_m)))) )
-    A[x] := [premise-list, c]
+    A[x] := [premise-list, g]
     return x
 
   (declare-rule x ((y_1 U_1) ... (y_n U_n))
@@ -2485,8 +2535,8 @@ RUN(C):
     return RUN( (declare-const s (Proof F)) )
 
   (step s F :rule r :premises (p_1 ... p_k) :args (t_1 ... t_n)):
-    if A[r] = [premise-list, c]
-      return RUN( (define s () (r t_1 ... t_n (ProofFromList c p_1 ... p_k))) )
+    if A[r] = [premise-list, g]
+      return RUN( (define s () (r t_1 ... t_n (ProofFromList g p_1 ... p_k))) )
     else
       return RUN( (define s () (r t_1 ... t_n p_1 ... p_k)) )
 

From bd071f22d8fcf75dd69573fce131fbf57775b619 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 13 Mar 2025 15:43:02 -0500
Subject: [PATCH 07/31] More

---
 user_manual.md | 135 +++++++++++++++++++++++++++----------------------
 1 file changed, 74 insertions(+), 61 deletions(-)

diff --git a/user_manual.md b/user_manual.md
index 088fd969..1d665535 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2169,6 +2169,8 @@ Notice this is only the case if the declaration of `r` does not involve `:assump
 
 # Formal Definition of Preprocessor
 
+This section defines a conversion from (full) Eunoia input syntax to a core logic.
+
 ### Core syntax of terms
 
 The category <term> denotes all terms and types.
@@ -2179,7 +2181,8 @@ In detail,
 
 The category <pterm> denotes "pre-terms", which include intermediate constructors that are used in the desugar mentioned below.
 Constructors specific to pre-terms are not expected to be returned by the desugar method for a well-formed term.
-In particular, this means that annotations e.g. `:implicit`, `:opaque`, `:var` should not appear anywhere by in function arguments, symbols introduced by the command `define` must be fully applied.
+In particular, this means that annotations e.g. `:implicit`, `:opaque`, `:var` should not appear anywhere by in function arguments, 
+symbols introduced by the command `define` must be fully applied.
 
 Pre-terms may appear as the second field of term annotations <annot>.
 
@@ -2201,6 +2204,8 @@ Pre-terms may appear as the second field of term annotations <annot>.
                      (Tuple <pterm>*) | (Lambda (Tuple <pterm>*) <pterm>)
 ```
 
+### Type 
+
 ### Parser State
 
 ```
@@ -2219,7 +2224,7 @@ The initial state can be understood by parsing the following background definiti
 (declare-const Bool Type)
 (declare-consts <boolean> Bool)
 
-; Definitions of applicaable eo::
+; TODO: Definitions of eo::
 ```
 
 ### Scoping of parameters
@@ -2248,13 +2253,16 @@ Parameters marked with the annotation `(x T :list)` are such that the attribute
 ### Desugaring of terms
 
 Takes as input the syntax given for a term. Returns a <pterm>.
-We use meta-variables `t_i, s_j` to denote terms, `T_i, U_j, V_k` to denote types (terms whose type is Type), `a_i, a_j` to denote annotations.
-We use `f` to denote a term of some function type.
+We use meta-variables `t_i, s_j, f, g, h` to denote terms, 
+`T_i, U_j, V_k` to denote types (terms whose type is Type), and
+`a_i, a_j` to denote annotations.
+We write `s` to denote a symbol.
 
 We assume the following helper methods:
 - `NAME(x)`: returns a string corresponding to the name of parameter or constant x.
 - `FREE_PARAMS(t)`: returns the set of parameters that occur as subterms of t.
 - `SUBS( t, [x_1, ..., x_n], [s_1, ..., s_n] )`: returns the result of replacing all occurrences of parameters `x_1, ..., x_n` by `s_1, ..., s_n` simultaneously.
+- `FRESH_CONST(s, T)`: constructs a constant with name `s` and type `T`.
 
 
 ```
@@ -2297,16 +2305,22 @@ DESUGAR(t):
 
   ;;; binders, definitions
 
-  (f ((x_1 U_1) ... (x_m U_m)) t_1 ... t_n), where A(f) = [binder, g]:
-    Let [v_1, ..., v_m] = [(eo::var NAME(x_1) U_1) ... (eo::var NAME(x_m) U_m)]
-    return DESUGAR( SUBS( (f (g x_1 ... x_m) t_1 ... t_n), [x_1, ..., x_m], [v_1, ..., v_m]) )
+  If A(f) = [binder, g]:
+
+    (f ((x_1 U_1) ... (x_m U_m)) t_1 ... t_n):
+      Let [v_1, ..., v_m] = [(eo::var NAME(x_1) U_1) ... (eo::var NAME(x_m) U_m)]
+      return DESUGAR( SUBS( (f (g x_1 ... x_m) t_1 ... t_n), [x_1, ..., x_m], [v_1, ..., v_m]) )
+
+  If A(f) = [let-binder, (Tuple lp ll)]:
+
+    (f ((x_1 s_1) ... (x_m s_m)) t):
+      Let [v_1, ..., v_m] = [(eo::var NAME(x_1) U_1) ... (eo::var NAME(x_m) U_m)]
+      return DESUGAR( SUBS( (f (ll (lp x_1 s_1) ... (lp x_m s_m)) t), [x_1, ..., x_m], [v_1, ..., v_m]) )
 
-  (f ((x_1 s_1) ... (x_m s_m)) t), where A(f) = [let-binder, (Tuple lp ll)]:
-    Let [v_1, ..., v_m] = [(eo::var NAME(x_1) U_1) ... (eo::var NAME(x_m) U_m)]
-    return DESUGAR( SUBS( (f (ll (lp x_1 s_1) ... (lp x_m s_m)) t), [x_1, ..., x_m], [v_1, ..., v_m]) )
+  If A(f) = [define, (Lambda (Tuple x_1 ... x_n) t)]:
 
-  (f t_1 ... t_n), where A(f) = [define, (Lambda (Tuple x_1 ... x_n) t)]:
-    return DESUGAR( SUBS( t, [x_1, ..., x_n], [t_1, ..., t_n]) )
+    (f t_1 ... t_n):
+      return DESUGAR( SUBS( t, [x_1, ..., x_n], [t_1, ..., t_n]) )
 
   (eo::define ((x_1 s_1) ... (x_m s_m)) t):
     return DESUGAR( SUBS( t, [x_1, ..., x_m], [s_1, ..., s_m]) )
@@ -2332,7 +2346,7 @@ DESUGAR(t):
     return (_# f DESUGAR(T) )
 
   (eo::as f (-> T_1 ... T_n T)), where S[NAME(f)] = [f_1, ..., f_m]:
-    Let [k_1, ..., k_n] be fresh constants of type [T_1, ..., T_n]
+    Let [k_1, ..., k_n] = [FRESH_CONST(k_1,T_1), ..., FRESH_CONST(k_n, T_n)]
     return DESUGAR(
       (eo::ite (eo::is_eq (eo::typeof (f_m k_1 ... k_n)) T) f_m
       ...
@@ -2352,84 +2366,83 @@ DESUGAR(t):
 
   ;;; n-ary kinds
 
-  ; where A(f) = [right-assoc-nil, g]:
+  If A(f) = [right-assoc-nil, g]:
 
-  (f t_1 ... t_n), where t_n != (Nil ...), A[t_n] != [list, Null]:
-    return DESUGAR( (f t_1 ... t_n (Nil f t_1 ... t_n)) )
+    (f t_1 ... t_n), where t_n != (Nil ...), A[t_n] != [list, Null]:
+      return DESUGAR( (f t_1 ... t_n (Nil f t_1 ... t_n)) )
 
-  (f t_1 ... t_n), where A[t_1] = [list, Null], n>1:
-    return (eo::list_concat f DESUGAR(t_1) DESUGAR( (f t_2 ... t_n) ))
+    (f t_1 ... t_n), where A[t_1] = [list, Null], n>1:
+      return (eo::list_concat f DESUGAR(t_1) DESUGAR( (f t_2 ... t_n) ))
 
-  (f t_1 ... t_n), where A[t_1] != [list, Null], n>1:
-    return (_ (_ f DESUGAR(t_1)) DESUGAR( (f t_2 ... t_n) ))
+    (f t_1 ... t_n), where A[t_1] != [list, Null], n>1:
+      return (_ (_ f DESUGAR(t_1)) DESUGAR( (f t_2 ... t_n) ))
 
-  (f t_1), where A(f) = [right-assoc-nil, g]:
-    return DESUGAR(t_1)
+    (f t_1), where A(f) = [right-assoc-nil, g]:
+      return DESUGAR(t_1)
 
-  ; where A(f) = [right-assoc, Null]:
+  If A(f) = [right-assoc, Null]:
 
-  (f t_1 ... t_n), where, n>1:
-    return (_ (_ f DESUGAR(t_1)) DESUGAR( (f t_2 ... t_n) ) )
+    (f t_1 ... t_n), where, n>1:
+      return (_ (_ f DESUGAR(t_1)) DESUGAR( (f t_2 ... t_n) ) )
 
-  (f t_1):
-    return DESUGAR(t_1)
+    (f t_1):
+      return DESUGAR(t_1)
 
-  ; where A(f) = [left-assoc-nil, g]:
+  If A(f) = [left-assoc-nil, g]:
 
-  (f t_1 ... t_n), where t_1 != (Nil ...), A[t_1] != [list, Null]:
-    return DESUGAR( (f (Nil f t_1 ... t_n) t_1 ... t_n) )
+    (f t_1 ... t_n), where t_1 != (Nil ...), A[t_1] != [list, Null]:
+      return DESUGAR( (f (Nil f t_1 ... t_n) t_1 ... t_n) )
 
-  (f t_1 ... t_n), where A[t_1] = [list, Null], n>1:
-    return (eo::list_concat f DESUGAR( (f t_2 ... t_n) ) DESUGAR(t_1))
+    (f t_1 ... t_n), where A[t_1] = [list, Null], n>1:
+      return (eo::list_concat f DESUGAR( (f t_2 ... t_n) ) DESUGAR(t_1))
 
-  (f t_1 ... t_n), where A[t_1] != [list, Null], n>1:
-    return (_ (_ f DESUGAR( (f t_2 ... t_n) )) DESUGAR(t_1))
+    (f t_1 ... t_n), where A[t_1] != [list, Null], n>1:
+      return (_ (_ f DESUGAR( (f t_2 ... t_n) )) DESUGAR(t_1))
 
-  (f t_1):
-    return DESUGAR(t_1)
+    (f t_1):
+      return DESUGAR(t_1)
 
-  ; where A(f) = [left-assoc, Null]:
+  If A(f) = [left-assoc, Null]:
 
-  (f t_1 ... t_n), n>1:
-    return (_ (_ f DESUGAR( (f t_2 ... t_n) )) DESUGAR(t_1))
+    (f t_1 ... t_n), n>1:
+      return (_ (_ f DESUGAR( (f t_2 ... t_n) )) DESUGAR(t_1))
 
-  (f t_1):
-    return DESUGAR(t_1)
+    (f t_1):
+      return DESUGAR(t_1)
 
-  ; where A(f) = [chainable, g]:
+  If A(f) = [chainable, g]:
 
-  (f t_1 t_2):
-    return (_ (_ f DESUGAR(t_1)) DESUGAR(t_2))
+    (f t_1 t_2):
+      return (_ (_ f DESUGAR(t_1)) DESUGAR(t_2))
 
-  (f t_1 ... t_n), n != 2:
-    return DESUGAR( (g (f t_1 t_2) (f t_2 t_3) ... (f t_{n-1} t_n)) )
+    (f t_1 ... t_n), n != 2:
+      return DESUGAR( (g (f t_1 t_2) (f t_2 t_3) ... (f t_{n-1} t_n)) )
 
-  ; where A(f) = [pairwise, g]:
+  If A(f) = [pairwise, g]:
 
-  (f t_1 t_2):
-    return (_ (_ f DESUGAR(t_1)) DESUGAR(t_2))
+    (f t_1 t_2):
+      return (_ (_ f DESUGAR(t_1)) DESUGAR(t_2))
 
-  (f t_1 ... t_n), n != 2:
-    return DESUGAR( (g (f t_1 t_2) (f t_1 t_3) ... (f t_2 t_3) ... (f t_{n-1} t_n)) )
+    (f t_1 ... t_n), n != 2:
+      return DESUGAR( (g (f t_1 t_2) (f t_1 t_3) ... (f t_2 t_3) ... (f t_{n-1} t_n)) )
 
   ;;; opaque
 
-  ; where A(f) = [opaque, (Tuple T_1 ... T_m)]:
+  If A(f) = [opaque, (Tuple T_1 ... T_m)]:
 
-  (f t_1 ... t_n), n = m:
-    return (_# (_# f DESUGAR(t_1)) ... DESUGAR(t_m))
+    (f t_1 ... t_n), n = m:
+      return (_# (_# f DESUGAR(t_1)) ... DESUGAR(t_m))
 
-  (f t_1 ... t_n), n > m:
-    return DESUGAR( ((_# (_# f DESUGAR(t_1)) ... DESUGAR(t_m)) t_{m+1} ... t_n) )
+    (f t_1 ... t_n), n > m:
+      return DESUGAR( ((_# (_# f DESUGAR(t_1)) ... DESUGAR(t_m)) t_{m+1} ... t_n) )
 
 
   ;;; programs, oracles, ordinary functions
 
-  (f t_1 ... t_n), where A(f) = [program, p]:
-    return (f DESUGAR(t_1) ... DESUGAR(t_n))
+  If A(f) = [program, p] or A(f) = [oracle, o]:
 
-  (f t_1 ... t_n), where A(f) = [oracle, s]:
-    return (f DESUGAR(t_1) ... DESUGAR(t_n))
+    (f t_1 ... t_n)
+      return (f DESUGAR(t_1) ... DESUGAR(t_n))
 
   (f t_1 ... t_n), n>1:
     return (_ DESUGAR( (f t_1 ... t_{n-1}) ) t_n)
@@ -2453,7 +2466,7 @@ RUN(C):
 
   (declare-const s T a):
     Let x = FRESH_CONST(s, DESUGAR(T))
-    A[x] := a
+    A[x] := [a.attr, DESUGAR(a.pterm)]
     S[s] += x
     return x
 

From 4565af63d89cdc84000a76471a7fdf7158a4b8c7 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 13 Mar 2025 16:12:53 -0500
Subject: [PATCH 08/31] More sketch

---
 user_manual.md | 39 ++++++++++++++++++++++++++++++++++-----
 1 file changed, 34 insertions(+), 5 deletions(-)

diff --git a/user_manual.md b/user_manual.md
index 1d665535..69198441 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2181,7 +2181,7 @@ In detail,
 
 The category <pterm> denotes "pre-terms", which include intermediate constructors that are used in the desugar mentioned below.
 Constructors specific to pre-terms are not expected to be returned by the desugar method for a well-formed term.
-In particular, this means that annotations e.g. `:implicit`, `:opaque`, `:var` should not appear anywhere by in function arguments, 
+In particular, this means that annotations e.g. `:implicit`, `:opaque`, `:var` should not appear anywhere but in function arguments, 
 symbols introduced by the command `define` must be fully applied.
 
 Pre-terms may appear as the second field of term annotations <annot>.
@@ -2195,7 +2195,7 @@ Pre-terms may appear as the second field of term annotations <annot>.
                       datatype | datatype-constructor | amb-datatype-constructor |
                       premise-list | none
   <annot>         := [ <attr>, <pterm> ]
-  <term>          := <param> | <const> | (eo::var <term> <term>) |
+  <term>          := <param> | <const> |
                       (-> <term> <term>) | (~> <term> <term>) | (--> <term>* <term>) |
                       (_ <term> <term>) | (_# <term> <term>) | (<prog-const> <term>*)
   <prog-const>    := <const> | eo::requires | eo::nil | eo::ite | eo::typeof | eo::is_eq
@@ -2225,6 +2225,9 @@ The initial state can be understood by parsing the following background definiti
 (declare-consts <boolean> Bool)
 
 ; TODO: Definitions of eo::
+
+; including eo::var, eo::list_concat
+
 ```
 
 ### Scoping of parameters
@@ -2477,8 +2480,8 @@ RUN(C):
     else
       return RUN( (declare-const s U :none) )
 
-  (declare-parameterized-const ((y_1 U_1) ... (y_n U_n)) T a):
-    TODO
+  (declare-parameterized-const s ((y_1 U_1) ... (y_n U_n)) T a):
+    return RUN( (declare-const s T a) )
 
   (declare-rule s ((y_1 U_1) ... (y_n U_n))
     :premises (p_1 ... p_k)
@@ -2549,7 +2552,8 @@ RUN(C):
 
   (step s F :rule r :premises (p_1 ... p_k) :args (t_1 ... t_n)):
     if A[r] = [premise-list, g]
-      return RUN( (define s () (r t_1 ... t_n (ProofFromList g p_1 ... p_k))) )
+      Let p = FRESH_CONST( p, DESUGAR( (Proof (g F_1 ... F_k) ) ) ), where p_1, ..., p_k have type (Proof F_1), ...., (Proof F_k).
+      return RUN( (define s () (r t_1 ... t_n p)) )
     else
       return RUN( (define s () (r t_1 ... t_n p_1 ... p_k)) )
 
@@ -2604,3 +2608,28 @@ RUN(C):
   (check-sat):
     ; do nothing
 ```
+
+### Type system
+
+```smt
+f : (~> u S)  t : T
+-------------------------- if SUBS(u, X, R) = t
+(_ f t) : EVAL( S, X, R )
+
+f : (-> U S)  t : T
+-------------------------- if SUBS(U, X, R) = Y
+(_ f t) : EVAL( S, X, R )
+
+f : (--> U_1 ... U_n S)  t_1 : T_1 ... t_n : T_n
+------------------------------------------------- if SUBS( (Tuple U_1 ... U_n), X, R) = (Tuple T_1 ... T_n)
+(_ f t_1 ... t_n) : EVAL( S, X, R )
+
+------------------------------------------
+c : EVAL( L(CATEGORY(c)), [eo::self], [c])
+
+```
+
+The type rule for `_#` is identical to those for `_`.
+The submethod `EVAL( t, [x_1, ..., x_n], [s_1, ..., s_n] )` 
+is the result of evaluating `t` in the context where parameters `[x_1, ..., x_n]`
+are bound to `[s_1, ..., s_n]`.

From 7d84eee2b5c522859a7d2e4d71d951ccdbdff908 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 13 Mar 2025 16:18:27 -0500
Subject: [PATCH 09/31] More

---
 user_manual.md | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/user_manual.md b/user_manual.md
index 69198441..ca0aef98 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2550,6 +2550,7 @@ RUN(C):
     ASSERT( F in Ax )
     return RUN( (declare-const s (Proof F)) )
 
+  ; TODO: improve handling of premise-list
   (step s F :rule r :premises (p_1 ... p_k) :args (t_1 ... t_n)):
     if A[r] = [premise-list, g]
       Let p = FRESH_CONST( p, DESUGAR( (Proof (g F_1 ... F_k) ) ) ), where p_1, ..., p_k have type (Proof F_1), ...., (Proof F_k).
@@ -2574,8 +2575,8 @@ RUN(C):
   (declare-oracle-fun s (T_1 ... T_n) T o):
     return RUN( (declare-const s (--> T_1 ... T_n T) :oracle o) )
 
-  (declare-consts cat T)
-    L[cat] := T
+  (declare-consts c T)
+    L[c] := T
 
   ;;; push/pop
 
@@ -2617,19 +2618,19 @@ f : (~> u S)  t : T
 (_ f t) : EVAL( S, X, R )
 
 f : (-> U S)  t : T
--------------------------- if SUBS(U, X, R) = Y
+-------------------------- if SUBS(U, X, R) = T
 (_ f t) : EVAL( S, X, R )
 
 f : (--> U_1 ... U_n S)  t_1 : T_1 ... t_n : T_n
 ------------------------------------------------- if SUBS( (Tuple U_1 ... U_n), X, R) = (Tuple T_1 ... T_n)
 (_ f t_1 ... t_n) : EVAL( S, X, R )
 
-------------------------------------------
+------------------------------------------ if CATEGORY(c) is defined
 c : EVAL( L(CATEGORY(c)), [eo::self], [c])
 
 ```
 
-The type rule for `_#` is identical to those for `_`.
-The submethod `EVAL( t, [x_1, ..., x_n], [s_1, ..., s_n] )` 
+The type rules for `_#` is identical to those for `_`.
+The submethod `EVAL( t, [x_1, ..., x_n], [r_1, ..., r_n] )` 
 is the result of evaluating `t` in the context where parameters `[x_1, ..., x_n]`
-are bound to `[s_1, ..., s_n]`.
+are bound to `[r_1, ..., r_n]`.

From 4f14d069e418a6b5d143d0ffe0d9cd95136c1c0f Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 13 Mar 2025 16:21:52 -0500
Subject: [PATCH 10/31] More

---
 user_manual.md | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

diff --git a/user_manual.md b/user_manual.md
index ca0aef98..2bc26d82 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2228,6 +2228,8 @@ The initial state can be understood by parsing the following background definiti
 
 ; including eo::var, eo::list_concat
 
+; eo::conclusion, eo::self?
+
 ```
 
 ### Scoping of parameters
@@ -2265,7 +2267,8 @@ We assume the following helper methods:
 - `NAME(x)`: returns a string corresponding to the name of parameter or constant x.
 - `FREE_PARAMS(t)`: returns the set of parameters that occur as subterms of t.
 - `SUBS( t, [x_1, ..., x_n], [s_1, ..., s_n] )`: returns the result of replacing all occurrences of parameters `x_1, ..., x_n` by `s_1, ..., s_n` simultaneously.
-- `FRESH_CONST(s, T)`: constructs a constant with name `s` and type `T`.
+- `FRESH_CONST(s, T)`: returns a fresh constant with name `s` and type `T`.
+- `CATEGORY(t)`: returns the `<lit-category>` for a term, if `t` is a literal.
 
 
 ```
@@ -2554,9 +2557,11 @@ RUN(C):
   (step s F :rule r :premises (p_1 ... p_k) :args (t_1 ... t_n)):
     if A[r] = [premise-list, g]
       Let p = FRESH_CONST( p, DESUGAR( (Proof (g F_1 ... F_k) ) ) ), where p_1, ..., p_k have type (Proof F_1), ...., (Proof F_k).
-      return RUN( (define s () (r t_1 ... t_n p)) )
+      Let res = SUBS( (r t_1 ... t_n p), [eo::conclusion], [F] )
+      return RUN( (define s () res) )
     else
-      return RUN( (define s () (r t_1 ... t_n p_1 ... p_k)) )
+      Let res = SUBS( (r t_1 ... t_n p_1 ... p_k), [eo::conclusion], [F] )
+      return RUN( (define s () res) )
 
   (program s ((x_1 U_1) ... (x_m U_m))
     (T_1 ... T_n) T
@@ -2625,8 +2630,8 @@ f : (--> U_1 ... U_n S)  t_1 : T_1 ... t_n : T_n
 ------------------------------------------------- if SUBS( (Tuple U_1 ... U_n), X, R) = (Tuple T_1 ... T_n)
 (_ f t_1 ... t_n) : EVAL( S, X, R )
 
------------------------------------------- if CATEGORY(c) is defined
-c : EVAL( L(CATEGORY(c)), [eo::self], [c])
+------------------------------------------ if CATEGORY(t) is defined
+t : EVAL( L(CATEGORY(t)), [eo::self], [t])
 
 ```
 

From 6b6489a98c1352ef8cc4aa2097d4a9974e389547 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 13 Mar 2025 16:40:59 -0500
Subject: [PATCH 11/31] Minor

---
 user_manual.md | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/user_manual.md b/user_manual.md
index 2bc26d82..a2ca89c3 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2183,8 +2183,7 @@ The category <pterm> denotes "pre-terms", which include intermediate constructor
 Constructors specific to pre-terms are not expected to be returned by the desugar method for a well-formed term.
 In particular, this means that annotations e.g. `:implicit`, `:opaque`, `:var` should not appear anywhere but in function arguments, 
 symbols introduced by the command `define` must be fully applied.
-
-Pre-terms may appear as the second field of term annotations <annot>.
+As an exception, we often use `Tuple` in the second field of term annotations <annot>.
 
 ```
   <lit-category>  := '<numeral>' | '<decimal>' | '<rational>' | '<binary>' | '<hexadecimal>' | '<string>'
@@ -2351,6 +2350,7 @@ DESUGAR(t):
   (as f T), where A(f) = [amb-datatype-constructor, s]:
     return (_# f DESUGAR(T) )
 
+  ; TODO: refactor base case
   (eo::as f (-> T_1 ... T_n T)), where S[NAME(f)] = [f_1, ..., f_m]:
     Let [k_1, ..., k_n] = [FRESH_CONST(k_1,T_1), ..., FRESH_CONST(k_n, T_n)]
     return DESUGAR(
@@ -2639,3 +2639,7 @@ The type rules for `_#` is identical to those for `_`.
 The submethod `EVAL( t, [x_1, ..., x_n], [r_1, ..., r_n] )` 
 is the result of evaluating `t` in the context where parameters `[x_1, ..., x_n]`
 are bound to `[r_1, ..., r_n]`.
+
+### Execution semantics
+
+TODO

From 8a59d9ed0268b0f835599d5f1e2caf11ea232736 Mon Sep 17 00:00:00 2001
From: Mallku Soldevila <mallkuernesto@gmail.com>
Date: Thu, 27 Mar 2025 12:38:16 -0300
Subject: [PATCH 12/31] minor fixes in Formal def. of preprocessor (#128)

Added some fixes to formatting syntax (e.g., <term> was changed to
`<term>`, so it can be displayed after processing the file).
---
 user_manual.md | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/user_manual.md b/user_manual.md
index a2ca89c3..482081e6 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2173,17 +2173,16 @@ This section defines a conversion from (full) Eunoia input syntax to a core logi
 
 ### Core syntax of terms
 
-The category <term> denotes all terms and types.
+The category `<term>` denotes all terms and types.
 This includes parameters, constants, and variables.
 In detail,
 `->` is function arrow, `~>` is quote arrow, `-->` is program arrow, 
 `_` is application and `_#` is opaque application.
 
-The category <pterm> denotes "pre-terms", which include intermediate constructors that are used in the desugar mentioned below.
+The category `<pterm>` denotes "pre-terms", which include intermediate constructors that are used in the desugar mentioned below.
 Constructors specific to pre-terms are not expected to be returned by the desugar method for a well-formed term.
-In particular, this means that annotations e.g. `:implicit`, `:opaque`, `:var` should not appear anywhere but in function arguments, 
-symbols introduced by the command `define` must be fully applied.
-As an exception, we often use `Tuple` in the second field of term annotations <annot>.
+In particular, this means that annotations (e.g. `:implicit`, `:opaque`, `:var`) should not appear anywhere but in function arguments. Symbols introduced by the command `define` must be fully applied.
+As an exception, we often use `Tuple` in the second field of term annotations `<annot>`.
 
 ```
   <lit-category>  := '<numeral>' | '<decimal>' | '<rational>' | '<binary>' | '<hexadecimal>' | '<string>'
@@ -2256,7 +2255,7 @@ Parameters marked with the annotation `(x T :list)` are such that the attribute
 
 ### Desugaring of terms
 
-Takes as input the syntax given for a term. Returns a <pterm>.
+Takes as input the syntax given for a term. Returns a `<pterm>`.
 We use meta-variables `t_i, s_j, f, g, h` to denote terms, 
 `T_i, U_j, V_k` to denote types (terms whose type is Type), and
 `a_i, a_j` to denote annotations.
@@ -2465,7 +2464,7 @@ DESUGAR(t):
 
 # Desugaring of commands
 
-Takes as input the syntax given for a command. Optionally returns a <const>.
+Takes as input the syntax given for a command. Optionally returns a `<const>`.
 
 ```
 RUN(C):
@@ -2635,7 +2634,7 @@ t : EVAL( L(CATEGORY(t)), [eo::self], [t])
 
 ```
 
-The type rules for `_#` is identical to those for `_`.
+The type rules for `_#` are identical to those for `_`.
 The submethod `EVAL( t, [x_1, ..., x_n], [r_1, ..., r_n] )` 
 is the result of evaluating `t` in the context where parameters `[x_1, ..., x_n]`
 are bound to `[r_1, ..., r_n]`.

From 33ee338568f4d633e55f9130ba2e60af640095a5 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 27 Mar 2025 10:49:46 -0500
Subject: [PATCH 13/31] Fixes, improvements

---
 user_manual.md | 17 +++++++----------
 1 file changed, 7 insertions(+), 10 deletions(-)

diff --git a/user_manual.md b/user_manual.md
index 482081e6..7a8399cd 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2500,12 +2500,10 @@ RUN(C):
     :args (t_1 ... t_l)
     :requires ((s_1 r_1) ... (s_1 s_m))
     :conclusion F):
-    x = RUN( 
+    return RUN( 
       (declare-const s (-> (Quote t_1) ... (Quote t_l)
                            (Proof x)
-                           (! F :requires (s_1 r_1) ... :requires (s_1 s_m)))) )
-    A[x] := [premise-list, g]
-    return x
+                           (! F :requires (s_1 r_1) ... :requires (s_1 s_m))) :premise-list g) )
 
   (declare-rule x ((y_1 U_1) ... (y_n U_n))
     :assumption a
@@ -2521,9 +2519,7 @@ RUN(C):
     return RUN( (declare-const s (-> U_1 ... U_n Type)) )
 
   (define s ((y_1 U_1) ... (y_n U_n)) t):
-    A[x] := [define, (Lambda (Tuple y_1 ... y_n) t)]
-    S[s] += x
-    return x
+    return RUN( (declare-const s (-> U_1 ... U_n (eo::typeof t)) :define (Lambda (Tuple y_1 ... y_n) t)) )
 
   (declare-datatype s () (par (U_1 ... U_n) ((c_1 (s_11 T_11) ... (s1m T_1m)) ... (c_n (s_n1 T_n1) ... (snm T_nm))))):
     Let DC = RUN( (declare-type s (U_1 ... U_n)) )
@@ -2565,13 +2561,14 @@ RUN(C):
   (program s ((x_1 U_1) ... (x_m U_m))
     (T_1 ... T_n) T
     (
-    ((s a_11 ... a_1n) r_0)
+    ((s a_11 ... a_1n) r_1)
     ...
     ((s a_k1 ... y_kn) r_k)
     )
   ):
-    return RUN( (declare-const s (--> T_1 ... T_n T)
-                  :program (Tuple (Tuple (f a_11 ... a_1n) r_0) ... (Tuple (f a_k1 ... y_kn) r_k))) )
+    Let p = RUN( (declare-const s (--> T_1 ... T_n T)) )
+    A[p] := [program, (Tuple (Tuple (p a_11 ... a_1n) r_1) ... (Tuple (p a_k1 ... y_kn) r_k))]
+    return p
   
   (declare-oracle-fun s () T o):
     return RUN( (declare-const s T :oracle o) )

From 19fa3cb3c9833e229c50d539a1b38be2130010e2 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 27 Mar 2025 12:02:25 -0500
Subject: [PATCH 14/31] More

---
 user_manual.md | 25 ++++++++++++++-----------
 1 file changed, 14 insertions(+), 11 deletions(-)

diff --git a/user_manual.md b/user_manual.md
index 7a8399cd..19b1ba8a 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2349,14 +2349,13 @@ DESUGAR(t):
   (as f T), where A(f) = [amb-datatype-constructor, s]:
     return (_# f DESUGAR(T) )
 
-  ; TODO: refactor base case
   (eo::as f (-> T_1 ... T_n T)), where S[NAME(f)] = [f_1, ..., f_m]:
     Let [k_1, ..., k_n] = [FRESH_CONST(k_1,T_1), ..., FRESH_CONST(k_n, T_n)]
     return DESUGAR(
       (eo::ite (eo::is_eq (eo::typeof (f_m k_1 ... k_n)) T) f_m
       ...
-      (eo::ite (eo::is_eq (eo::typeof (f_2 k_1 ... k_n)) T) f_2
-        (eo::requires (eo::typeof (f_1 k_1 ... k_n)) T f_1)...)) )
+      (eo::ite (eo::is_eq (eo::typeof (f_1 k_1 ... k_n)) T) f_1
+        f_m ...)) )  ; In practice, we give a warning in this case if the types fail for all overloads.
 
   ;;; pre-term operators
 
@@ -2382,7 +2381,7 @@ DESUGAR(t):
     (f t_1 ... t_n), where A[t_1] != [list, Null], n>1:
       return (_ (_ f DESUGAR(t_1)) DESUGAR( (f t_2 ... t_n) ))
 
-    (f t_1), where A(f) = [right-assoc-nil, g]:
+    (f t_1):
       return DESUGAR(t_1)
 
   If A(f) = [right-assoc, Null]:
@@ -2442,20 +2441,24 @@ DESUGAR(t):
       return DESUGAR( ((_# (_# f DESUGAR(t_1)) ... DESUGAR(t_m)) t_{m+1} ... t_n) )
 
 
-  ;;; programs, oracles, ordinary functions
+  ;;; programs, oracles
 
   If A(f) = [program, p] or A(f) = [oracle, o]:
 
-    (f t_1 ... t_n)
+    (f t_1 ... t_n):
       return (f DESUGAR(t_1) ... DESUGAR(t_n))
 
-  (f t_1 ... t_n), n>1:
-    return (_ DESUGAR( (f t_1 ... t_{n-1}) ) t_n)
+  ;;; ordinary functions
+
+  if A(f) = [none, Null}:
 
-  (f t_1):
-    return (_ f DESUGAR(t_1))
+    (f t_1 ... t_n), n>1:
+      return (_ DESUGAR( (f t_1 ... t_{n-1}) ) t_n)
+
+    (f t_1):
+      return (_ f DESUGAR(t_1))
 
-  ;;; base case
+  ;;; atomic terms
 
   t:
     return t

From 7e298108ae94d0c713c5abc9c95ff96b258f5a70 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 27 Mar 2025 12:06:06 -0500
Subject: [PATCH 15/31] More

---
 user_manual.md | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/user_manual.md b/user_manual.md
index 19b1ba8a..a5689aab 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2267,7 +2267,7 @@ We assume the following helper methods:
 - `SUBS( t, [x_1, ..., x_n], [s_1, ..., s_n] )`: returns the result of replacing all occurrences of parameters `x_1, ..., x_n` by `s_1, ..., s_n` simultaneously.
 - `FRESH_CONST(s, T)`: returns a fresh constant with name `s` and type `T`.
 - `CATEGORY(t)`: returns the `<lit-category>` for a term, if `t` is a literal.
-
+- `RUN(C)`: returns the constant declared by command `C`, or `Null` if the command did not declare a constant.
 
 ```
 DESUGAR(t):
@@ -2467,7 +2467,7 @@ DESUGAR(t):
 
 # Desugaring of commands
 
-Takes as input the syntax given for a command. Optionally returns a `<const>`.
+Takes as input the syntax given for a command. Either returns a `<const>` or the `Null` term.
 
 ```
 RUN(C):
@@ -2501,12 +2501,12 @@ RUN(C):
   (declare-rule s ((y_1 U_1) ... (y_n U_n))
     :premise-list x g
     :args (t_1 ... t_l)
-    :requires ((s_1 r_1) ... (s_1 s_m))
+    :requires ((s_1 r_1) ... (s_m r_m))
     :conclusion F):
     return RUN( 
       (declare-const s (-> (Quote t_1) ... (Quote t_l)
                            (Proof x)
-                           (! F :requires (s_1 r_1) ... :requires (s_1 s_m))) :premise-list g) )
+                           (! F :requires (s_1 r_1) ... :requires (s_m r_m))) :premise-list g) )
 
   (declare-rule x ((y_1 U_1) ... (y_n U_n))
     :assumption a
@@ -2581,6 +2581,7 @@ RUN(C):
 
   (declare-consts c T)
     L[c] := T
+    return Null
 
   ;;; push/pop
 
@@ -2609,9 +2610,11 @@ RUN(C):
 
   (assert F):
     Ax := Ax ++ [F]
+    return Null
 
   (check-sat):
     ; do nothing
+    return Null
 ```
 
 ### Type system

From 8856c3095420cb8206455d1d3ff182c9572ad93d Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 31 Mar 2025 10:18:34 -0500
Subject: [PATCH 16/31] More accurate overloading

---
 user_manual.md | 41 +++++++++++++++++++++++++----------------
 1 file changed, 25 insertions(+), 16 deletions(-)

diff --git a/user_manual.md b/user_manual.md
index a5689aab..e9292371 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2307,6 +2307,31 @@ DESUGAR(t):
   (-> T_0):
     return DESUGAR( T_0 )
 
+  ;;; special operators
+
+  (_ t_1 ... t_n):
+    return DESUGAR( (t_1 ... t_n) )
+
+  (as f T), where A(f) = [amb-datatype-constructor, s]:
+    return (_# f DESUGAR(T) )
+
+  (eo::as f (-> T_1 ... T_n T)), where S[NAME(f)] = [f_1, ..., f_m]:
+    Let [k_1, ..., k_n] = [FRESH_CONST("", T_1), ..., FRESH_CONST("", T_n)]
+    return
+      (eo::ite DESUGAR( (eo::is_eq (eo::typeof (f_m k_1 ... k_n)) T) ) f_m
+      ...
+      (eo::ite DESUGAR( (eo::is_eq (eo::typeof (f_1 k_1 ... k_n)) T) ) f_1
+        (eo::as f_m DESUGAR( (-> T_1 ... T_n T) ) ...)) )  ; eo::as is unprocessed, will be a type error.
+
+  ;;; overloaded functions
+
+  (f t_1 ... t_n), where S[NAME(f)] = [f_1, ..., f_m], m>1:
+    return DESUGAR(
+      (_ (eo::ite (eo::is_eq (eo::typeof (f_m t_1 ... t_n)) T) f_m
+         ...
+         (eo::ite (eo::is_eq (eo::typeof (f_1 t_1 ... t_n)) T) f_1
+            f_m ...)) t_1 ... t_n)  )  ; Defaults to most recent if type checking fails for all overloads, we give a warning in this case.
+
   ;;; binders, definitions
 
   If A(f) = [binder, g]:
@@ -2341,22 +2366,6 @@ DESUGAR(t):
                       ((s p_n y_1 ... y_k) r_n)))) )
     return DESUGAR( (h t y_1 ... y_k) )
 
-  ;;; special operators
-
-  (_ t_1 ... t_n):
-    return DESUGAR( (t_1 ... t_n) )
-
-  (as f T), where A(f) = [amb-datatype-constructor, s]:
-    return (_# f DESUGAR(T) )
-
-  (eo::as f (-> T_1 ... T_n T)), where S[NAME(f)] = [f_1, ..., f_m]:
-    Let [k_1, ..., k_n] = [FRESH_CONST(k_1,T_1), ..., FRESH_CONST(k_n, T_n)]
-    return DESUGAR(
-      (eo::ite (eo::is_eq (eo::typeof (f_m k_1 ... k_n)) T) f_m
-      ...
-      (eo::ite (eo::is_eq (eo::typeof (f_1 k_1 ... k_n)) T) f_1
-        f_m ...)) )  ; In practice, we give a warning in this case if the types fail for all overloads.
-
   ;;; pre-term operators
 
   (Opaque t_1):

From a8eebef4e01ac1d6c581f7bafffae4e8c119b96b Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 31 Mar 2025 10:20:26 -0500
Subject: [PATCH 17/31] Minor

---
 user_manual.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/user_manual.md b/user_manual.md
index e9292371..949611b7 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2321,16 +2321,16 @@ DESUGAR(t):
       (eo::ite DESUGAR( (eo::is_eq (eo::typeof (f_m k_1 ... k_n)) T) ) f_m
       ...
       (eo::ite DESUGAR( (eo::is_eq (eo::typeof (f_1 k_1 ... k_n)) T) ) f_1
-        (eo::as f_m DESUGAR( (-> T_1 ... T_n T) ) ...)) )  ; eo::as is unprocessed, will be a type error.
+        (eo::as f_m DESUGAR( (-> T_1 ... T_n T) ) ...)) )  ; Otherwise, eo::as is unprocessed, will be a type error.
 
   ;;; overloaded functions
 
-  (f t_1 ... t_n), where S[NAME(f)] = [f_1, ..., f_m], m>1:
+  (f t_1 ... t_n), where S[NAME(f)] = [f_1, ..., f_m] and m>1:
     return DESUGAR(
       (_ (eo::ite (eo::is_eq (eo::typeof (f_m t_1 ... t_n)) T) f_m
          ...
          (eo::ite (eo::is_eq (eo::typeof (f_1 t_1 ... t_n)) T) f_1
-            f_m ...)) t_1 ... t_n)  )  ; Defaults to most recent if type checking fails for all overloads, we give a warning in this case.
+            f_m ...)) t_1 ... t_n)  )  ; Otherwise, defaults to most recent if type checking fails for all overloads, we give a warning in this case.
 
   ;;; binders, definitions
 

From 7afcf75ad3051c18a0150bcc09d56bb15965187d Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 31 Mar 2025 10:34:11 -0500
Subject: [PATCH 18/31] More

---
 user_manual.md | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/user_manual.md b/user_manual.md
index 949611b7..77f3141b 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2323,15 +2323,6 @@ DESUGAR(t):
       (eo::ite DESUGAR( (eo::is_eq (eo::typeof (f_1 k_1 ... k_n)) T) ) f_1
         (eo::as f_m DESUGAR( (-> T_1 ... T_n T) ) ...)) )  ; Otherwise, eo::as is unprocessed, will be a type error.
 
-  ;;; overloaded functions
-
-  (f t_1 ... t_n), where S[NAME(f)] = [f_1, ..., f_m] and m>1:
-    return DESUGAR(
-      (_ (eo::ite (eo::is_eq (eo::typeof (f_m t_1 ... t_n)) T) f_m
-         ...
-         (eo::ite (eo::is_eq (eo::typeof (f_1 t_1 ... t_n)) T) f_1
-            f_m ...)) t_1 ... t_n)  )  ; Otherwise, defaults to most recent if type checking fails for all overloads, we give a warning in this case.
-
   ;;; binders, definitions
 
   If A(f) = [binder, g]:

From b2e545a06e24cb7e047724c8259e8948b3ef2c30 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 31 Mar 2025 10:36:52 -0500
Subject: [PATCH 19/31] More

---
 user_manual.md | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

diff --git a/user_manual.md b/user_manual.md
index 77f3141b..17c7303b 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2255,7 +2255,8 @@ Parameters marked with the annotation `(x T :list)` are such that the attribute
 
 ### Desugaring of terms
 
-Takes as input the syntax given for a term. Returns a `<pterm>`.
+Below, we define a method `DESUGAR` which takes as input the syntax given for a term.
+It returns a `<pterm>`.
 We use meta-variables `t_i, s_j, f, g, h` to denote terms, 
 `T_i, U_j, V_k` to denote types (terms whose type is Type), and
 `a_i, a_j` to denote annotations.
@@ -2269,6 +2270,18 @@ We assume the following helper methods:
 - `CATEGORY(t)`: returns the `<lit-category>` for a term, if `t` is a literal.
 - `RUN(C)`: returns the constant declared by command `C`, or `Null` if the command did not declare a constant.
 
+Prior to calling `DESUGAR`, we assume all applications of overloaded functions are handled as follows.
+Assume `f` is overloaded such that `S[NAME(f)] = [f_1, ..., f_m]` where `m>1`.
+We replace all function applications of the form `(f t_1 ... t_n)` with:
+```
+(eo::ite (eo::is_eq (eo::typeof (f_m t_1 ... t_n)) T) (f_m t_1 ... t_n)
+...
+(eo::ite (eo::is_eq (eo::typeof (f_1 t_1 ... t_n)) T) (f_1 t_1 ... t_n)
+  (f_m t_1 ... t_n)) ...)
+```
+where notice that we use the most recently bound function symbol `f_m` if type-checking fails for all overloads.
+In this case, the reduced term `(f_m t_1 ... t_n)` will be ill-typed.
+
 ```
 DESUGAR(t):
 
@@ -2467,7 +2480,9 @@ DESUGAR(t):
 
 # Desugaring of commands
 
-Takes as input the syntax given for a command. Either returns a `<const>` or the `Null` term.
+Below, we define a method `RUN` which takes as input the syntax given for a command. 
+This method either returns a `<const>`, indicating the constant that was declared by the command,
+or otherwise returns the `Null` term.
 
 ```
 RUN(C):

From 9d8434b97d0600c2fcc6712c864182ff8dcafb1f Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 31 Mar 2025 11:07:13 -0500
Subject: [PATCH 20/31] More

---
 user_manual.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/user_manual.md b/user_manual.md
index 17c7303b..a5ff4293 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2268,7 +2268,7 @@ We assume the following helper methods:
 - `SUBS( t, [x_1, ..., x_n], [s_1, ..., s_n] )`: returns the result of replacing all occurrences of parameters `x_1, ..., x_n` by `s_1, ..., s_n` simultaneously.
 - `FRESH_CONST(s, T)`: returns a fresh constant with name `s` and type `T`.
 - `CATEGORY(t)`: returns the `<lit-category>` for a term, if `t` is a literal.
-- `RUN(C)`: returns the constant declared by command `C`, or `Null` if the command did not declare a constant.
+- `RUN(C)`: returns the constant declared by command `C`, or `Null` if the command did not declare a constant. A comprehensive definition of this method is given later.
 
 Prior to calling `DESUGAR`, we assume all applications of overloaded functions are handled as follows.
 Assume `f` is overloaded such that `S[NAME(f)] = [f_1, ..., f_m]` where `m>1`.
@@ -2334,7 +2334,7 @@ DESUGAR(t):
       (eo::ite DESUGAR( (eo::is_eq (eo::typeof (f_m k_1 ... k_n)) T) ) f_m
       ...
       (eo::ite DESUGAR( (eo::is_eq (eo::typeof (f_1 k_1 ... k_n)) T) ) f_1
-        (eo::as f_m DESUGAR( (-> T_1 ... T_n T) ) ...)) )  ; Otherwise, eo::as is unprocessed, will be a type error.
+        (eo::as f_m DESUGAR( (-> T_1 ... T_n T) ) ...)) )  ; Otherwise, eo::as is unprocessed.
 
   ;;; binders, definitions
 

From 143c2920c9b13dc4d6c4fd1d4ffea7aa13c1932e Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 31 Mar 2025 11:17:03 -0500
Subject: [PATCH 21/31] More

---
 user_manual.md | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

diff --git a/user_manual.md b/user_manual.md
index a5ff4293..836b6855 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2194,8 +2194,8 @@ As an exception, we often use `Tuple` in the second field of term annotations `<
                       premise-list | none
   <annot>         := [ <attr>, <pterm> ]
   <term>          := <param> | <const> |
-                      (-> <term> <term>) | (~> <term> <term>) | (--> <term>* <term>) |
-                      (_ <term> <term>) | (_# <term> <term>) | (<prog-const> <term>*)
+                      (-> <term> <term>) | (~> <term> <term>) | (--> <term>+ <term>) |
+                      (_ <term> <term>) | (_# <term> <term>) | (<prog-const> <term>+)
   <prog-const>    := <const> | eo::requires | eo::nil | eo::ite | eo::typeof | eo::is_eq
 
   <pterm>         := <term> | Null | (Opaque <pterm>) | (Quote <pterm>) | (Nil <pterm>*) |
@@ -2571,10 +2571,10 @@ RUN(C):
     if A[r] = [premise-list, g]
       Let p = FRESH_CONST( p, DESUGAR( (Proof (g F_1 ... F_k) ) ) ), where p_1, ..., p_k have type (Proof F_1), ...., (Proof F_k).
       Let res = SUBS( (r t_1 ... t_n p), [eo::conclusion], [F] )
-      return RUN( (define s () res) )
+      return RUN( (define s () res :type (Proof F)) )
     else
       Let res = SUBS( (r t_1 ... t_n p_1 ... p_k), [eo::conclusion], [F] )
-      return RUN( (define s () res) )
+      return RUN( (define s () res :type (Proof F)) )
 
   (program s ((x_1 U_1) ... (x_m U_m))
     (T_1 ... T_n) T
@@ -2634,6 +2634,7 @@ RUN(C):
 
 ### Type system
 
+
 ```smt
 f : (~> u S)  t : T
 -------------------------- if SUBS(u, X, R) = t
@@ -2657,6 +2658,11 @@ The submethod `EVAL( t, [x_1, ..., x_n], [r_1, ..., r_n] )`
 is the result of evaluating `t` in the context where parameters `[x_1, ..., x_n]`
 are bound to `[r_1, ..., r_n]`.
 
+By convention, we assume
+a term is well typed only if its type does not contain an application of a program or builtin evaluation operator.
+In other words, all type rules above assume the side condition that `T` respects this restriction if `t : T` is concluded.
+Moreover we assume that all types are fully evaluated when assigned to atomic terms.
+
 ### Execution semantics
 
 TODO

From de296684e8ddc7943049e907140947ac32b23489 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 30 May 2025 07:33:40 -0500
Subject: [PATCH 22/31] Minor

---
 user_manual.md | 27 ++++++---------------------
 1 file changed, 6 insertions(+), 21 deletions(-)

diff --git a/user_manual.md b/user_manual.md
index ed5d6d2a..b6bc34b9 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2386,27 +2386,12 @@ DESUGAR(t):
 
   ;;; annotations
 
-  (! T :implicit a_1 ... a_n):
-    return DESUGAR( (! Null a_1 ... a_n) )
-
-  (! T :opaque a_1 ... a_n), where T != Null:
-    return DESUGAR( (! (Opaque T) a_1 ... a_n) )
-
-  (! T :requires (t1 t2) a_1 ... a_n), where T != Null:
-    return DESUGAR( (! (eo::requires t_1 t_2 T) a_1 ... a_n) )
-
-  (! T :var x a_1 ... a_n), where T != Null, (Quote U) for any U:
-    Let x is a fresh parameter of type T.
-    return DESUGAR( (! (Quote x) a_1 ... a_n) )
-
-  (! t):
+  ; term attributes are ignored
+  (! t a_1 ... a_n):
     return DESUGAR(t)
 
   ;;; function types
 
-  (-> Null T_1 ... T_n):
-    return DESUGAR( (-> T_1 ... T_n) )
-
   (-> (eo::requires s1 s2 T_0) T_1 ... T_n):
     return DESUGAR( (-> T_0 (eo::requires s1 s2 (-> T_1 ... T_n))) )
 
@@ -2477,15 +2462,15 @@ DESUGAR(t):
   (Quote t_1):
     return (Quote DESUGAR(t_1))
 
-  (Nil f t_1 ... t_n):
-    return (eo::nil f DESUGAR(t_1) ... DESUGAR(t_n))
+  (Nil f T):
+    return (eo::nil f DESUGAR(T))
 
   ;;; n-ary kinds
 
   If A(f) = [right-assoc-nil, g]:
 
     (f t_1 ... t_n), where t_n != (Nil ...), A[t_n] != [list, Null]:
-      return DESUGAR( (f t_1 ... t_n (Nil f t_1 ... t_n)) )
+      return DESUGAR( (f t_1 ... t_n (Nil f (eo::typeof t_1))) )
 
     (f t_1 ... t_n), where A[t_1] = [list, Null], n>1:
       return (eo::list_concat f DESUGAR(t_1) DESUGAR( (f t_2 ... t_n) ))
@@ -2507,7 +2492,7 @@ DESUGAR(t):
   If A(f) = [left-assoc-nil, g]:
 
     (f t_1 ... t_n), where t_1 != (Nil ...), A[t_1] != [list, Null]:
-      return DESUGAR( (f (Nil f t_1 ... t_n) t_1 ... t_n) )
+      return DESUGAR( (f (Nil f (eo::typeof t_1)) t_1 ... t_n) )
 
     (f t_1 ... t_n), where A[t_1] = [list, Null], n>1:
       return (eo::list_concat f DESUGAR( (f t_2 ... t_n) ) DESUGAR(t_1))

From a8bef5ed473291afef2dd66e96763f39063d6300 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 30 May 2025 09:31:59 -0500
Subject: [PATCH 23/31] More refactor

---
 user_manual.md | 39 ++++++++++++++-------------------------
 1 file changed, 14 insertions(+), 25 deletions(-)

diff --git a/user_manual.md b/user_manual.md
index b6bc34b9..21af5e58 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2584,38 +2584,27 @@ RUN(C):
     else
       return RUN( (declare-const s U :none) )
 
-  (declare-parameterized-const s ((y_1 U_1) ... (y_n U_n)) T a):
+  (declare-parameterized-const s () T a):
     return RUN( (declare-const s T a) )
 
-  (declare-rule s ((y_1 U_1) ... (y_n U_n))
-    :premises (p_1 ... p_k)
-    :args (t_1 ... t_l)
-    :requires ((s_1 r_1) ... (s_1 s_m))
-    :conclusion F):
-    return RUN( 
-      (declare-const s (-> (Quote t_1) ... (Quote t_l)
-                           (Proof p_1) ... (Proof p_k)
-                           (! F :requires (s_1 r_1) ... :requires (s_1 s_m)))) )
+  (declare-parameterized-const s ((y_1 U_1) ... (y_n U_n :implicit)) T a):
+    return RUN( (declare-parameterized-const s ((y_1 U_1) ... (y_{n-1} U_{n-1})) T a) )
+
+  (declare-parameterized-const s ((y_1 U_1) ... (y_n U_n :requires t s)) T a):
+    return RUN( (declare-parameterized-const s ((y_1 U_1) ... (y_n U_n)) (eo::requires t s T) a) )
 
   (declare-rule s ((y_1 U_1) ... (y_n U_n))
-    :premise-list x g
+    [:assumption a]?
+    [:premises (p_1 ... p_k) | :premise-list pl g]
     :args (t_1 ... t_l)
     :requires ((s_1 r_1) ... (s_m r_m))
-    :conclusion F):
-    return RUN( 
-      (declare-const s (-> (Quote t_1) ... (Quote t_l)
-                           (Proof x)
-                           (! F :requires (s_1 r_1) ... :requires (s_m r_m))) :premise-list g) )
-
-  (declare-rule x ((y_1 U_1) ... (y_n U_n))
-    :assumption a
-    :args (t_1 ... t_l)
-    :requires ((s_1 r_1) ... (s_1 s_m))
-    :conclusion F):
+    [:conclusion F | :conclusion-explicit Fx]):
     return RUN( 
       (declare-const s (-> (Quote t_1) ... (Quote t_l)
-                           (Proof p_1) ... (Proof p_k) (Proof a)
-                           (! F :requires (s_1 r_1) ... :requires (s_1 s_m)))) )
+                           [(Proof p_1) ... (Proof p_k) | (Proof pl)]
+                           [(Quote a)]? [(Quote Fx)]?
+                           (eo::requires s_1 r_1 ... (eo::requires s_m r_m
+                           [F | Fx])))) )
 
   (declare-type s (U_1 ... U_n)):
     return RUN( (declare-const s (-> U_1 ... U_n Type)) )
@@ -2661,7 +2650,7 @@ RUN(C):
       return RUN( (define s () res :type (Proof F)) )
 
   (program s ((x_1 U_1) ... (x_m U_m))
-    (T_1 ... T_n) T
+    :signature (T_1 ... T_n) T
     (
     ((s a_11 ... a_1n) r_1)
     ...

From e1ea7b278062b5441e8480a4ca2b125cf40c81b6 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 30 May 2025 09:52:45 -0500
Subject: [PATCH 24/31] More

---
 user_manual.md | 55 ++++++++++++++++++++++++++++++++++----------------
 1 file changed, 38 insertions(+), 17 deletions(-)

diff --git a/user_manual.md b/user_manual.md
index 21af5e58..16d56a2f 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2297,7 +2297,7 @@ As an exception, we often use `Tuple` in the second field of term annotations `<
                       (_ <term> <term>) | (_# <term> <term>) | (<prog-const> <term>+)
   <prog-const>    := <const> | eo::requires | eo::nil | eo::ite | eo::typeof | eo::is_eq
 
-  <pterm>         := <term> | Null | (Opaque <pterm>) | (Quote <pterm>) | (Nil <pterm>*) |
+  <pterm>         := <term> | (Opaque <pterm>) | (Quote <pterm>) | (Nil <pterm>*) |
                      (Tuple <pterm>*) | (Lambda (Tuple <pterm>*) <pterm>)
 ```
 
@@ -2587,30 +2587,51 @@ RUN(C):
   (declare-parameterized-const s () T a):
     return RUN( (declare-const s T a) )
 
-  (declare-parameterized-const s ((y_1 U_1) ... (y_n U_n :implicit)) T a):
-    return RUN( (declare-parameterized-const s ((y_1 U_1) ... (y_{n-1} U_{n-1})) T a) )
+  (declare-parameterized-const s ((y_1 U_1 a_1) ... (y_n U_n a_n :list)) T a):
+    return RUN( (declare-parameterized-const s ((y_1 U_1 a_1) ... (y_n U_n a_n)) T a) )
 
-  (declare-parameterized-const s ((y_1 U_1) ... (y_n U_n :requires t s)) T a):
-    return RUN( (declare-parameterized-const s ((y_1 U_1) ... (y_n U_n)) (eo::requires t s T) a) )
+  (declare-parameterized-const s ((y_1 U_1 a_1) ... (y_n U_n a_n :requires t s)) T a):
+    return RUN( (declare-parameterized-const s ((y_1 U_1 a_1) ... (y_n U_n a_n)) (eo::requires t s T) a) )
+
+  (declare-parameterized-const s ((y_1 U_1 a_1) ... (y_n U_n :implicit)) T a):
+    return RUN( (declare-parameterized-const s ((y_1 U_1 a_1) ... (y_{n-1} U_{n-1} a_{n-1})) T a) )
+
+  (declare-parameterized-const s ((y_1 U_1 a_1) ... (y_n U_n :opaque)) T a):
+    return RUN( (declare-parameterized-const s ((y_1 U_1 a_1) ... (y_{n-1} U_{n-1} a_{n-1})) (-> (Opaque (Quote y_n)) T) a) )
+
+  (declare-parameterized-const s ((y_1 U_1 a_1) ... (y_n U_n)) T a):
+    return RUN( (declare-parameterized-const s ((y_1 U_1 a_1) ... (y_{n-1} U_{n-1} a_{n-1})) (-> (Quote y_n) T) a) )
+
+  (declare-type s (U_1 ... U_n)):
+    return RUN( (declare-const s (-> U_1 ... U_n Type)) )
+
+  (define s ((y_1 U_1 a_1) ... (y_n U_n a_n)) t):
+    return RUN( (define s ((y_1 U_1 a_1) ... (y_n U_n a_n)) t :define (Lambda (Tuple) t)) )
+
+  (define s ((y_1 U_1 a_1) ... (y_n U_n a_n :list)) t :define (Lambda (Tuple z_1 ... z_m) t)):
+    return RUN( (define s ((y_1 U_1 a_1) ... (y_n U_n a_n)) t :define (Lambda (Tuple z_1 ... z_m) t)) )
+
+  (define s ((y_1 U_1 a_1) ... (y_n U_n :implicit)) t :define (Lambda (Tuple z_1 ... z_m) t)):
+    return RUN( (define s ((y_1 U_1 a_1) ... (y_{n-1} U_{n-1} a_{n-1})) t :define (Lambda (Tuple z_1 ... z_m) t)) )
+
+  (define s ((y_1 U_1 a_1) ... (y_n U_n)) t :define (Lambda (Tuple z_1 ... z_m) t)):
+    return RUN( (define s ((y_1 U_1 a_1) ... (y_{n-1} U_{n-1} a_{n-1})) t :define (Lambda (Tuple y_n z_1 ... z_m) t)) )
+
+  (define s () t :define (Lambda (Tuple z_1 ... z_m) t)):
+    return RUN( (declare-const s (-> (eo::typeof z_1)  ... (eo::typeof z_m) (eo::typeof t)) :define (Lambda (Tuple z_1 ... z_m) t)) )
 
   (declare-rule s ((y_1 U_1) ... (y_n U_n))
     [:assumption a]?
-    [:premises (p_1 ... p_k) | :premise-list pl g]
+    [:premises (p_1 ... p_k) | :premise-list pl_p pl_g]
     :args (t_1 ... t_l)
     :requires ((s_1 r_1) ... (s_m r_m))
-    [:conclusion F | :conclusion-explicit Fx]):
-    return RUN( 
+    [:conclusion F | :conclusion-explicit F_x]):
+    return RUN(
       (declare-const s (-> (Quote t_1) ... (Quote t_l)
-                           [(Proof p_1) ... (Proof p_k) | (Proof pl)]
+                           [(Proof p_1) ... (Proof p_k) | (Proof pl_p)]
                            [(Quote a)]? [(Quote Fx)]?
                            (eo::requires s_1 r_1 ... (eo::requires s_m r_m
-                           [F | Fx])))) )
-
-  (declare-type s (U_1 ... U_n)):
-    return RUN( (declare-const s (-> U_1 ... U_n Type)) )
-
-  (define s ((y_1 U_1) ... (y_n U_n)) t):
-    return RUN( (declare-const s (-> U_1 ... U_n (eo::typeof t)) :define (Lambda (Tuple y_1 ... y_n) t)) )
+                           [F | Fx]))) :rule (Tuple a? F_x? pl_g?)) )
 
   (declare-datatype s () (par (U_1 ... U_n) ((c_1 (s_11 T_11) ... (s1m T_1m)) ... (c_n (s_n1 T_n1) ... (snm T_nm))))):
     Let DC = RUN( (declare-type s (U_1 ... U_n)) )
@@ -2624,7 +2645,7 @@ RUN(C):
         A[dc_i] := [amb-datatype-constructor, sels]
       else
         Let dc_i = RUN( (declare-const c_i (-> T_i1 ... T_im D)) )
-        A[dc_i] := [amb-datatype-constructor, sels]
+        A[dc_i] := [datatype-constructor, sels]
     A[DC] := [datatype, (Tuple dc_1 ... dc_n)]
     return DC
 

From ee4e80314f7605e9d47144952d480235761655fc Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 30 May 2025 10:18:19 -0500
Subject: [PATCH 25/31] More

---
 user_manual.md | 62 ++++++++++++++++++++++++++------------------------
 1 file changed, 32 insertions(+), 30 deletions(-)

diff --git a/user_manual.md b/user_manual.md
index 16d56a2f..0d6a1398 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2312,6 +2312,8 @@ As an exception, we often use `Tuple` in the second field of term annotations `<
   A : maps <const> to <annot>.
   ; Assertions (formulas provided in assert commands).
   Ax : a list of <term>.
+  ; Local assertions (formulas pushed via assume-push).
+  Axl : a list of <term>.
   ; Category types, maps literal categories to their types.
   L : maps <lit-category> to <term>
 ```
@@ -2621,17 +2623,40 @@ RUN(C):
     return RUN( (declare-const s (-> (eo::typeof z_1)  ... (eo::typeof z_m) (eo::typeof t)) :define (Lambda (Tuple z_1 ... z_m) t)) )
 
   (declare-rule s ((y_1 U_1) ... (y_n U_n))
-    [:assumption a]?
+    [:assumption q]?
     [:premises (p_1 ... p_k) | :premise-list pl_p pl_g]
     :args (t_1 ... t_l)
-    :requires ((s_1 r_1) ... (s_m r_m))
+    :requires ((s_1 r_1) ... (s_m r_m) a_s)
     [:conclusion F | :conclusion-explicit F_x]):
     return RUN(
       (declare-const s (-> (Quote t_1) ... (Quote t_l)
                            [(Proof p_1) ... (Proof p_k) | (Proof pl_p)]
-                           [(Quote a)]? [(Quote Fx)]?
+                           [(Quote q)]? [(Quote Fx)]?
                            (eo::requires s_1 r_1 ... (eo::requires s_m r_m
-                           [F | Fx]))) :rule (Tuple a? F_x? pl_g?)) )
+                           [F | Fx]))) :rule (Tuple q? pl_g? F_x?)) )
+
+  (assume s F):
+    ASSERT( F in Ax )
+    return RUN( (declare-const s (Proof F)) )
+
+  (assume-push s F)
+    Axl.push(F)
+    return RUN( (declare-const s (Proof F)) )
+
+  ([step | step-pop] s F? :rule r :premises (p_1 ... p_k) :args (t_1 ... t_n)):
+    ASSERT( A[r] = [rule, (Tuple q pl_g F_x)] )   ; r must be a proof rule
+    ASSERT( (q == Null) iff this.cmd == step )    ; step-pop used iff r has an assumption
+    ASSERT( (F_x == Null) or (F != Null) )        ; conclusion provided if r has an explicit conclusion
+    Let res = (
+      if pl_g == Null
+        (r t_1 ... t_n [Axl.pop()]? [F]? p_1 ... p_k)
+      else
+        Assume p_1, ..., p_k have type (Proof F_1), ...., (Proof F_k).
+        Let pl = RUN( (declare-const tmp DESUGAR( (Proof (g F_1 ... F_k) ) ) ) ).
+        (r t_1 ... t_n [Axl.pop()]? [F]? pl) )
+    return RUN( (define s () res :type (Proof F)) )
+      where the most recent assertion is popped via Axl.pop() and provided if q is not Null,
+        and F is provided if F_x is not null
 
   (declare-datatype s () (par (U_1 ... U_n) ((c_1 (s_11 T_11) ... (s1m T_1m)) ... (c_n (s_n1 T_n1) ... (snm T_nm))))):
     Let DC = RUN( (declare-type s (U_1 ... U_n)) )
@@ -2656,20 +2681,6 @@ RUN(C):
   (declare-datatypes ...):
     TODO
 
-  (assume s F):
-    ASSERT( F in Ax )
-    return RUN( (declare-const s (Proof F)) )
-
-  ; TODO: improve handling of premise-list
-  (step s F :rule r :premises (p_1 ... p_k) :args (t_1 ... t_n)):
-    if A[r] = [premise-list, g]
-      Let p = FRESH_CONST( p, DESUGAR( (Proof (g F_1 ... F_k) ) ) ), where p_1, ..., p_k have type (Proof F_1), ...., (Proof F_k).
-      Let res = SUBS( (r t_1 ... t_n p), [eo::conclusion], [F] )
-      return RUN( (define s () res :type (Proof F)) )
-    else
-      Let res = SUBS( (r t_1 ... t_n p_1 ... p_k), [eo::conclusion], [F] )
-      return RUN( (define s () res :type (Proof F)) )
-
   (program s ((x_1 U_1) ... (x_m U_m))
     :signature (T_1 ... T_n) T
     (
@@ -2678,9 +2689,9 @@ RUN(C):
     ((s a_k1 ... y_kn) r_k)
     )
   ):
-    Let p = RUN( (declare-const s (--> T_1 ... T_n T)) )
-    A[p] := [program, (Tuple (Tuple (p a_11 ... a_1n) r_1) ... (Tuple (p a_k1 ... y_kn) r_k))]
-    return p
+    return RUN(
+      (declare-const s (--> T_1 ... T_n T)
+        :program (Tuple (Tuple (Tuple a_11 ... a_1n) r_1) ... (Tuple (Tuple a_k1 ... y_kn) r_k))) )
   
   (declare-oracle-fun s () T o):
     return RUN( (declare-const s T :oracle o) )
@@ -2692,15 +2703,6 @@ RUN(C):
     L[c] := T
     return Null
 
-  ;;; push/pop
-
-  (assume-push s F)
-    return RUN( (declare-const s (Proof F)) )
-
-  (step-pop s F :rule r :premises (p_1 ... p_k) :args (t_1 ... t_n)), where (assume-push s G)
-  is the assumption that is being popped:
-    TODO
-
   ;;; SMT-LIB
 
   (declare-fun s () T):

From b80b1b2bb8d22c414a514ea2aab8c74072a49e84 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 30 May 2025 10:23:54 -0500
Subject: [PATCH 26/31] MOre

---
 user_manual.md | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/user_manual.md b/user_manual.md
index 0d6a1398..e8a38987 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2287,10 +2287,9 @@ As an exception, we often use `Tuple` in the second field of term annotations `<
   <lit-category>  := '<numeral>' | '<decimal>' | '<rational>' | '<binary>' | '<hexadecimal>' | '<string>'
   <attr>          :=  right-assoc-nil | right-assoc | left-assoc | left-assoc-nil |
                       chainable | pairwise | binder | let-binder |
-                      program | oracle |
-                      list | opaque |
+                      program | oracle | amb | list | opaque |
                       datatype | datatype-constructor | amb-datatype-constructor |
-                      premise-list | none
+                      rule | none
   <annot>         := [ <attr>, <pterm> ]
   <term>          := <param> | <const> |
                       (-> <term> <term>) | (~> <term> <term>) | (--> <term>+ <term>) |
@@ -2327,7 +2326,7 @@ The initial state can be understood by parsing the following background definiti
 
 ; including eo::var, eo::list_concat
 
-; eo::conclusion, eo::self?
+; eo::self?
 
 ```
 
@@ -2581,7 +2580,9 @@ RUN(C):
 
   (declare-const s T):
     Let U = DESUGAR(T)
-    if U is (-> (Opaque U_1) ... (-> (Opaque U_n) V) ... )
+    if U is ambiguous with return type R:
+      return RUN( (declare-const s (-> (Quote R) T) :amb) )
+    else if U is (-> (Opaque U_1) ... (-> (Opaque U_n) V) ... )
       return RUN( (declare-const s (-> U_1 ... U_n V) :opaque (Tuple U_1 ... U_n)) )
     else
       return RUN( (declare-const s U :none) )

From 5f18e7549afd9d9ac6b0343f9e6917c024f7645d Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 30 May 2025 11:30:29 -0500
Subject: [PATCH 27/31] Minor fixes

---
 user_manual.md | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/user_manual.md b/user_manual.md
index e8a38987..b3a8e6ae 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2632,16 +2632,16 @@ RUN(C):
     return RUN(
       (declare-const s (-> (Quote t_1) ... (Quote t_l)
                            [(Proof p_1) ... (Proof p_k) | (Proof pl_p)]
-                           [(Quote q)]? [(Quote Fx)]?
+                           [(Quote q)]? [(Quote F_x)]?
                            (eo::requires s_1 r_1 ... (eo::requires s_m r_m
-                           [F | Fx]))) :rule (Tuple q? pl_g? F_x?)) )
+                           [F | F_x]))) :rule (Tuple q? pl_g? F_x?)) )
 
   (assume s F):
-    ASSERT( F in Ax )
+    ASSERT( DESUGAR( F ) in Ax )   ; the assumption must have occurred in an assert command
     return RUN( (declare-const s (Proof F)) )
 
   (assume-push s F)
-    Axl.push(F)
+    Axl.push( DESUGAR( F ) )
     return RUN( (declare-const s (Proof F)) )
 
   ([step | step-pop] s F? :rule r :premises (p_1 ... p_k) :args (t_1 ... t_n)):
@@ -2713,15 +2713,15 @@ RUN(C):
     return RUN( (declare-const x (-> T_1 ... T_n T)) )
 
   (define-fun x () T t):
-    Ax := Ax ++ [DESUGAR( (= x t) )]  ; assumes user definition of =.
+    Ax.push(DESUGAR( (= x t) ))    ; assumes user definition of =.
     return RUN( (declare-const x T) )
 
   (define-fun x ((y_1 U_1) ... (y_n U_n)) T t):
-    Ax := Ax ++ [DESUGAR( (= x (lambda ((y_1 U_1) ... (y_n U_n)) t)) )] ; assumes user definition of =, lambda.
+    Ax.push(DESUGAR( (= x (lambda ((y_1 U_1) ... (y_n U_n)) t)) )) ; assumes user definition of =, lambda.
     return RUN( (declare-const x (-> U_1 ... U_n T)) )
 
   (assert F):
-    Ax := Ax ++ [F]
+    Ax.push(DESUGAR( F ))
     return Null
 
   (check-sat):

From 90db5073ce7b6c4ef54432861113edd696a94e82 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 30 May 2025 11:31:37 -0500
Subject: [PATCH 28/31] Minor

---
 user_manual.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/user_manual.md b/user_manual.md
index b3a8e6ae..5d6c2658 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2266,7 +2266,7 @@ If no conlusion is provided, then the type attribute is not specified.
 Notice this is only the case if the declaration of `r` does not involve `:assumption` or `:premise-list`.
 
 
-# Formal Definition of Preprocessor
+# Formal Definition of Parser of Ethos
 
 This section defines a conversion from (full) Eunoia input syntax to a core logic.
 

From a776192c2c0df2575a412a38a82edbcdb973e2ea Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 30 May 2025 11:35:58 -0500
Subject: [PATCH 29/31] More

---
 user_manual.md | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

diff --git a/user_manual.md b/user_manual.md
index 5d6c2658..05619341 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2374,9 +2374,9 @@ Prior to calling `DESUGAR`, we assume all applications of overloaded functions a
 Assume `f` is overloaded such that `S[NAME(f)] = [f_1, ..., f_m]` where `m>1`.
 We replace all function applications of the form `(f t_1 ... t_n)` with:
 ```
-(eo::ite (eo::is_eq (eo::typeof (f_m t_1 ... t_n)) T) (f_m t_1 ... t_n)
+(eo::ite (eo::eq (eo::typeof (f_m t_1 ... t_n)) T) (f_m t_1 ... t_n)
 ...
-(eo::ite (eo::is_eq (eo::typeof (f_1 t_1 ... t_n)) T) (f_1 t_1 ... t_n)
+(eo::ite (eo::eq (eo::typeof (f_1 t_1 ... t_n)) T) (f_1 t_1 ... t_n)
   (f_m t_1 ... t_n)) ...)
 ```
 where notice that we use the most recently bound function symbol `f_m` if type-checking fails for all overloads.
@@ -2416,9 +2416,9 @@ DESUGAR(t):
   (eo::as f (-> T_1 ... T_n T)), where S[NAME(f)] = [f_1, ..., f_m]:
     Let [k_1, ..., k_n] = [FRESH_CONST("", T_1), ..., FRESH_CONST("", T_n)]
     return
-      (eo::ite DESUGAR( (eo::is_eq (eo::typeof (f_m k_1 ... k_n)) T) ) f_m
+      (eo::ite DESUGAR( (eo::eq (eo::typeof (f_m k_1 ... k_n)) T) ) f_m
       ...
-      (eo::ite DESUGAR( (eo::is_eq (eo::typeof (f_1 k_1 ... k_n)) T) ) f_1
+      (eo::ite DESUGAR( (eo::eq (eo::typeof (f_1 k_1 ... k_n)) T) ) f_1
         (eo::as f_m DESUGAR( (-> T_1 ... T_n T) ) ...)) )  ; Otherwise, eo::as is unprocessed.
 
   ;;; binders, definitions
@@ -2437,7 +2437,7 @@ DESUGAR(t):
 
   If A(f) = [define, (Lambda (Tuple x_1 ... x_n) t)]:
 
-    (f t_1 ... t_n):
+    (f t_1 ... t_n), n>0:
       return DESUGAR( SUBS( t, [x_1, ..., x_n], [t_1, ..., t_n]) )
 
   (eo::define ((x_1 s_1) ... (x_m s_m)) t):
@@ -2558,6 +2558,11 @@ DESUGAR(t):
 
   ;;; atomic terms
 
+  If A(t) = [define, (Lambda (Tuple) s)]:
+
+    t:
+      return s
+
   t:
     return t
 ```

From 876735a7a75e87e67787f24b776701d0d00142b9 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 30 May 2025 11:42:07 -0500
Subject: [PATCH 30/31] Minor

---
 user_manual.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/user_manual.md b/user_manual.md
index 05619341..9cce6661 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2344,6 +2344,9 @@ Parameters introduced at the term level e.g. by `eo::match`, `eo::define`, or as
 As an exception,
 parameters marked `(x T :implicit)` are only in scope in the remainder of parsing the parameter list, 
 and are omitted from the parameter list after they are parsed.
+All parameters marked `(x T :list)` are such that `A[x]` is set to `[list, Null]`.
+For simplicity of presentation, for parameters with multiple attributes,
+we assume that attributes with keywords `:list` and `:requires` come after the other attributes.
 
 Parameters are generated in several other special contexts.
 In parameteric datatype definitions `(par (U_1 ... U_n) (<cons-dec>+))`, 

From cabfc89fb1682335fce37a6ef49fded340b6b651 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 30 May 2025 11:45:58 -0500
Subject: [PATCH 31/31] More

---
 user_manual.md | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/user_manual.md b/user_manual.md
index 9cce6661..0d8c96c1 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -2294,9 +2294,10 @@ As an exception, we often use `Tuple` in the second field of term annotations `<
   <term>          := <param> | <const> |
                       (-> <term> <term>) | (~> <term> <term>) | (--> <term>+ <term>) |
                       (_ <term> <term>) | (_# <term> <term>) | (<prog-const> <term>+)
-  <prog-const>    := <const> | eo::requires | eo::nil | eo::ite | eo::typeof | eo::is_eq
+  <prog-const>    := <const> | eo::requires | eo::nil | eo::ite | eo::typeof | eo::eq
 
-  <pterm>         := <term> | (Opaque <pterm>) | (Quote <pterm>) | (Nil <pterm>*) |
+  ; "pre-terms", used during parsing
+  <pterm>         := <term> | (Opaque <pterm>) | (Quote <pterm>) | (Nil <pterm> <pterm>) |
                      (Tuple <pterm>*) | (Lambda (Tuple <pterm>*) <pterm>)
 ```
 
@@ -2304,6 +2305,8 @@ As an exception, we often use `Tuple` in the second field of term annotations `<
 
 ### Parser State
 
+The following summarizes the state of the parser.
+
 ```
   ; Symbol table.
   S : maps strings to a list of <term>.
@@ -2317,7 +2320,7 @@ As an exception, we often use `Tuple` in the second field of term annotations `<
   L : maps <lit-category> to <term>
 ```
 
-The initial state can be understood by parsing the following background definitions:
+The initial state is the result of running the following background definitions:
 ```
 (declare-const Bool Type)
 (declare-consts <boolean> Bool)