OAI/Computability/TypeSystem/Signed.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PureTypeSystem.SignedInterpretation.Vector line 15
  2. def OAI.PureTypeSystem.SignedInterpretation.value line 17
  3. theorem OAI.PureTypeSystem.SignedInterpretation.value_candidate line 20
  4. theorem OAI.PureTypeSystem.SignedInterpretation.value_forward line 26
  5. theorem OAI.PureTypeSystem.SignedInterpretation.value_backward line 34
  6. def OAI.PureTypeSystem.SignedInterpretation.stepCandidate line 42
  7. def OAI.PureTypeSystem.SignedInterpretation.step line 54
  8. theorem OAI.PureTypeSystem.SignedInterpretation.step_monotone line 58
  9. def OAI.PureTypeSystem.SignedInterpretation.operator line 117
  10. def OAI.PureTypeSystem.SignedInterpretation.fixed line 120
  11. def OAI.PureTypeSystem.SignedInterpretation.actual line 122
  12. theorem OAI.PureTypeSystem.SignedInterpretation.actual_candidate line 124
  13. theorem OAI.PureTypeSystem.SignedInterpretation.actual_outside line 127
  14. theorem OAI.PureTypeSystem.SignedInterpretation.actual_product line 130
  15. abbrev OAI.PureTypeSystem.SignedInterpretation.Environment line 149
  16. def OAI.PureTypeSystem.SignedInterpretation.R line 151
  17. theorem OAI.PureTypeSystem.SignedInterpretation.R_candidate line 155
  18. theorem OAI.PureTypeSystem.SignedInterpretation.R_outside line 161
  19. theorem OAI.PureTypeSystem.SignedInterpretation.R_conversion line 169
  20. theorem OAI.PureTypeSystem.SignedInterpretation.actual_sort line 184
  21. theorem OAI.PureTypeSystem.SignedInterpretation.R_sort line 191
  22. theorem OAI.PureTypeSystem.SignedInterpretation.R_weakening line 195
  23. theorem OAI.PureTypeSystem.SignedInterpretation.R_before line 204
  24. theorem OAI.PureTypeSystem.SignedInterpretation.actual_raw_product line 219

    Source documentation

    The actual fixed point tests precisely every raw argument; normalization of its codomain commutes with this specialization by confluence.

    theorem actual_raw_product {Γ : List (Expr S)} {D E : Expr S} {s : S}
    (hp : HasType P Γ (.pi D E) (.sort s)) (e : Environment Ω Γ)
    (ha : Ω.profile ((Expr.pi D E).subst e.val) ∈ C) (h : Expr S) :
    h ∈ actual Ω hC hw hno ((Expr.pi D E).subst e.val).normalForm ↔
    h ∈ Top Ω ((Expr.pi D E).subst e.val).normalForm ∧
      ∀ n, n ∈ actual Ω hC hw hno (D.subst e.val).normalForm →
        Expr.app h n ∈ actual Ω hC hw hno (E.subst (Expr.extend e.val n)).normalForm := by
…

    Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.HasType, OAI.PureTypeSystem.SignedInterpretation.Environment, OAI.PureTypeSystem.SignedInterpretation.actual, OAI.PureTypeSystem.Expr.extend

  25. theorem OAI.PureTypeSystem.SignedInterpretation.product_intro line 274
  26. theorem OAI.PureTypeSystem.SignedInterpretation.specialization line 297
  27. def OAI.PureTypeSystem.SignedInterpretation.componentInterface line 313