OAI/Computability/TypeSystem/ObservationCandidates.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PureTypeSystem.ObservationValues.normal_subst_eq line 15

    Source documentation

    Normalizing the generic expression before a raw typed substitution leaves its actual normal form unchanged.

    theorem normal_subst_eq {Γ : List (Expr S)} {A : Expr S} {s : S}
    (hA : HasType P Γ A (.sort s)) (e : Environment (hw := hw) Ω C hno Γ) :
…

    Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.HasType, OAI.PureTypeSystem.ObservationValues.Environment

  2. def OAI.PureTypeSystem.ObservationValues.normalRead line 22
  3. theorem OAI.PureTypeSystem.ObservationValues.normalRead_eq line 28
  4. theorem OAI.PureTypeSystem.ObservationValues.preEvaluate_read_cast_expr line 34
  5. theorem OAI.PureTypeSystem.ObservationValues.normalRead_eq_of_nf line 41
  6. theorem OAI.PureTypeSystem.ObservationValues.normalRead_congr line 48
  7. theorem OAI.PureTypeSystem.ObservationValues.read_outside line 55
  8. theorem OAI.PureTypeSystem.ObservationValues.normalRead_outside line 61
  9. theorem OAI.PureTypeSystem.ObservationValues.normalRead_sort line 69
  10. def OAI.PureTypeSystem.ObservationValues.R line 79

    Source documentation

    The component entry is generic-normal Read; other generic profiles and unsorted literal expected sorts use exactly typed top.

    noncomputable def R {Γ : List (Expr S)} (A : Expr S) (e : Environment (hw := hw) Ω C hno Γ) : Set (Expr S) :=
…

    Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.ObservationValues.Environment

  11. theorem OAI.PureTypeSystem.ObservationValues.R_candidate line 85
  12. theorem OAI.PureTypeSystem.ObservationValues.R_of_sorted line 94
  13. theorem OAI.PureTypeSystem.ObservationValues.R_outside line 101
  14. theorem OAI.PureTypeSystem.ObservationValues.R_sort line 110
  15. def OAI.PureTypeSystem.ObservationValues.Environment.ofImages line 120
  16. def OAI.PureTypeSystem.ObservationValues.Environment.Ext line 134
  17. theorem OAI.PureTypeSystem.ObservationValues.Environment.Ext.reindexed line 138
  18. theorem OAI.PureTypeSystem.ObservationValues.Environment.cons_ext line 144
  19. theorem OAI.PureTypeSystem.ObservationValues.Environment.extend_exists line 149
  20. theorem OAI.PureTypeSystem.ObservationValues.Environment.ext_data line 153
  21. theorem OAI.PureTypeSystem.ObservationValues.Environment.Ext.payload line 159
  22. theorem OAI.PureTypeSystem.ObservationValues.Environment.Ext.eq_cons line 165
  23. theorem OAI.PureTypeSystem.ObservationValues.R_sorted_conversion line 177
  24. theorem OAI.PureTypeSystem.ObservationValues.R_normalForm line 189
  25. theorem OAI.PureTypeSystem.ObservationValues.R_conversion line 196
  26. theorem OAI.PureTypeSystem.ObservationValues.normalRead_weaken line 202
  27. theorem OAI.PureTypeSystem.ObservationValues.R_weakening line 214
  28. theorem OAI.PureTypeSystem.ObservationValues.normalRead_recontext line 227
  29. theorem OAI.PureTypeSystem.ObservationValues.R_recontext line 236
  30. theorem OAI.PureTypeSystem.ObservationValues.R_eq_normalRead_relevant line 259
  31. theorem OAI.PureTypeSystem.ObservationValues.R_eq_read_normal line 268
  32. theorem OAI.PureTypeSystem.ObservationValues.R_eq_read_good line 274
  33. theorem OAI.PureTypeSystem.ObservationValues.normal_product_candidate line 281
  34. theorem OAI.PureTypeSystem.ObservationValues.normal_product_iff line 293
  35. theorem OAI.PureTypeSystem.ObservationValues.Environment.Ext.argument line 362
  36. theorem OAI.PureTypeSystem.ObservationValues.Environment.Ext.convert_domain line 368
  37. theorem OAI.PureTypeSystem.ObservationValues.normalRead_compatible line 384
  38. theorem OAI.PureTypeSystem.ObservationValues.R_compatible line 390
  39. theorem OAI.PureTypeSystem.ObservationValues.R_binder_conversion line 402
  40. theorem OAI.PureTypeSystem.ObservationValues.product_iff line 423
  41. theorem OAI.PureTypeSystem.ObservationValues.product_intro line 466
  42. theorem OAI.PureTypeSystem.ObservationValues.product_argument_active line 484
  43. theorem OAI.PureTypeSystem.ObservationValues.R_instantiate_normal line 497
  44. theorem OAI.PureTypeSystem.ObservationValues.specialization line 531
  45. def OAI.PureTypeSystem.ObservationValues.componentInterface line 591

    Source documentation

    The actual observation interpretation, with arbitrary typed raw images and all matching payload extensions. No component interface law is assumed.

    noncomputable def componentInterface (hC : IsComponent (PrimaryEdge P) C) : ComponentInterface Ω hw C where
…

    Mentions: OAI.PureTypeSystem.IsComponent, OAI.PureTypeSystem.PrimaryEdge, OAI.PureTypeSystem.ComponentInterface