progress on the Names API

2023-08-07 21:15:48 +02:00
parent 9fcee982e5
commit 531e2c2dd2
36 changed files with 220 additions and 22 deletions
@@ -16,4 +16,10 @@ lin FullName gn sn = {
      a = {n = Sg; p = P3}
    } ;

+lin UsePN pn = { 
+      s = \\c => pn.s ! c;
+      h = pn.h;
+      a = {n = pn.n; p = P3}
+    } ;
+
 }