struct field projector and project struct builtin

Lampe/Lampe/Builtin/Struct.lean

@@ -35,7 +35,7 @@ def tupleNth {fieldTps : List Tp} (tpl : Tp.denote p (.tuple nameOpt fieldTps))
     | _, Fin.mk (.succ n') _ => tupleNth tpl.snd (Fin.mk n' _) (nameOpt := nameOpt)
 
 inductive projectTupleOmni : Omni where
-| mk {p st} {fieldTps : List Tp} {n : Fin fieldTps.length} {tpl Q} :
+| mk {p st} {n : Fin fieldTps.length} {tpl Q} :
   Q (some (st, tupleNth tpl n)) →
   projectTupleOmni p st [.tuple _ fieldTps] (fieldTps.get n) h![tpl] Q
 
@@ -55,4 +55,27 @@ def projectTuple : Builtin := {
     repeat apply Exists.intro <;> tauto
 }
 
+def structFieldProjector (fieldTps : List Tp) := (fieldName : String) → Fin fieldTps.length
+
+inductive projectStructOmni : Omni where
+| mk {p st} {proj : structFieldProjector fieldTps} {fieldName : String} {tpl Q} :
+  Q (some (st, tupleNth tpl (proj fieldName))) →
+  projectStructOmni p st [.tuple _ fieldTps] (fieldTps.get (proj fieldName)) h![tpl] Q
+
+def projectStruct : Builtin := {
+  omni := projectStructOmni
+  conseq := by
+    unfold omni_conseq
+    intros
+    cases_type projectStructOmni
+    tauto
+  frame := by
+    unfold omni_frame
+    intros
+    cases_type projectStructOmni
+    constructor
+    simp only
+    repeat apply Exists.intro <;> tauto
+}
+
 end Lampe.Builtin