OAI/Analysis/MatrixSigning/Realization/ListRealization.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.Realization.listCode_append line 12
2. lemma OAI.CurrentKS.Realization.listCode_cons line 16
3. lemma OAI.CurrentKS.Realization.listCode_nil line 19
4. def OAI.CurrentKS.Realization.consList line 21
5. def OAI.CurrentKS.Realization.appendList line 25
6. def OAI.CurrentKS.Realization.reverseBody line 36
7. lemma OAI.CurrentKS.Realization.fold_cons line 40
8. def OAI.CurrentKS.Realization.reverseList line 45
9. def OAI.CurrentKS.Realization.mapCtxUpdate line 49
10. def OAI.CurrentKS.Realization.mapCtxBody line 52
11. lemma OAI.CurrentKS.Realization.fold_mapCtx line 61
12. def OAI.CurrentKS.Realization.Realizes.mapCtx line 72