Fix F-Default

appendix/full-rules-set.typ

@@ -17,7 +17,7 @@ All the following rules are to be considered for a given program $P$, where fiel
   M-Type-2, "",
   M-Args, "",
   M-Args-2, "",
-  F-Type, ""
+  F-Default, ""
 )
 
 == Well-Formed Contexts

chapters/5-Annotation-System.typ

@@ -53,11 +53,11 @@ Finally, statements and expressions are pretty similar to Kotlin.
   M-Type-2, "",
   M-Args, "",
   M-Args-2, "",
-  F-Type, ""
+  F-Default, ""
 )
 
 Given a program $P$, M-Type rules define a function taking a method name and returning its type. Similarly, M-Args rules define a function taking a method name and returning its arguments. In order to derive these rules, the method must be contained within $P$.
-For simplicity, it is assumed that in $P$, fields within the same class, as well as across different classes, have distinct names. This assumption simplifies the definition of the F-Type rule, which defines a function that returns the type of a given field access.
+For simplicity, it is assumed that in $P$, fields within the same class, as well as across different classes, have distinct names. This assumption simplifies the definition of the F-Default rule, which defines a function that returns the type of a given field.
 
 #example[
   Given a method: $ m(x: unique borrowed, y: shared): unique $
@@ -247,7 +247,7 @@ $ root : p -> p $
 
 Lookup rules define a (partial) function that, given a well-formed context, returns the annotations associated with a given path
 
-When the path is explicitly contained within the context, the function returns the corresponding annotation. If a field access ($p.f$) is not explicitly present in the context, the function returns the annotations specified in the class declaration. This concept, formalized by Lookup-Default, is crucial as it ensures that contexts remain finite, even when handling recursive classes. However, if a variable ($x$) is not present in the context, its lookup cannot be derived.
+When the path is explicitly contained within the context, the function returns the corresponding annotation. If a field access ($p.f$) is not explicitly present in the context, the function returns the annotations specified in the class declaration containing $f$. This concept, formalized by Lookup-Default, is crucial as it ensures that contexts remain finite, even when handling recursive classes. However, if a variable ($x$) is not present in the context, its lookup cannot be derived.
 
 It is important to note that the lookup function returns the annotations associated with a path based on the context or the class declaration, rather than determining the actual ownership status of that path.
 
@@ -517,9 +517,9 @@ Finally @call-sup-ok-2 shows that it is possible to call `h` by passing `x` and
   use_g_h(x: unique) {
     begin_use_g_h;
         ⊣ Δ = x: unique
-      g(x, x); // ok, uniqueness is also preserved since both the args are borrowed
+    g(x, x); // ok, uniqueness is also preserved since both the args are borrowed
         ⊣ Δ = x: unique
-      h(x, x); // ok, but uniqueness is lost after normalization
+    h(x, x); // ok, but uniqueness is lost after normalization
         ⊣ Δ = x: shared
   }
   ```

config/utils.typ

@@ -20,6 +20,7 @@
 #let alias = "alias"
 #let root = "root"
 #let type = "type"
+#let default = "default"
 #let mtype = "m-type"
 #let ctx = "ctx"
 #let norm = "normalize"

vars/rules/base.typ

@@ -23,9 +23,9 @@
   rule(label: "M-Args-2", $args(m) = x_0, ..., x_n$),
 )
 
-#let F-Type = prooftree(
+#let F-Default = prooftree(
   axiom($class C(overline(f': alpha'_f), f: alpha_f, overline(f'': alpha''_f)) in P$),
-  rule(label: "F-Type", $type(p.f) = alpha_f$),
+  rule(label: "F-Default", $default(f) = alpha_f$),
 )
 
 // ****************** Context ******************
@@ -79,9 +79,7 @@
 
 
 #let Lookup-Default = prooftree(
-  // axiom($type(p) = C$),
-  // axiom($class C(overline(f': alpha'_f), f: alpha, overline(f'': alpha''_f)) in P$),
-  axiom($type(p.f) = alpha$),
+  axiom($default(f) = alpha$),
   rule(label: "Lookup-Default", $dot inangle(p.f) = alpha$),
 )