OAI/Computability/TypeSystem/Candidates.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PureTypeSystem.Candidates.ActualType line 14

    Source documentation

    Source actual types: a normal sorted expression, or a literal sort.

    def ActualType (T : Expr S) : Prop :=
…

    Mentions: OAI.PureTypeSystem.Expr

  2. def OAI.PureTypeSystem.Candidates.Top line 17
  3. inductive OAI.PureTypeSystem.Candidates.TestedStack line 21

    Source documentation

    Tests follow the exact normal successive types, not other typings.

    inductive TestedStack : Expr S → List (Expr S) → Prop
  | nil (T) : TestedStack T []
  | cons {D E n ns} : n ∈ Top Ω D →
      TestedStack (E.instantiate n).normalForm ns → TestedStack (.pi D E) (n :: ns)

    Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.Candidates.Top

  4. def OAI.PureTypeSystem.Candidates.Ground line 26
  5. theorem OAI.PureTypeSystem.Candidates.TestedStack.sn line 33
  6. theorem OAI.PureTypeSystem.Candidates.TestedStack.forall_sn line 38
  7. theorem OAI.PureTypeSystem.Candidates.ground_le_top line 51
  8. theorem OAI.PureTypeSystem.Candidates.sort_ground_eq_top line 55
  9. theorem OAI.PureTypeSystem.Candidates.var_ground line 63
  10. theorem OAI.PureTypeSystem.Candidates.ground_application line 66
  11. def OAI.PureTypeSystem.Candidates.ExpansionClosed line 74

    Source documentation

    Head expansion, with exact typing and SN of every annotation/spine component.

    def ExpansionClosed (Ω : ContextTower P) (T : Expr S) (C : Set (Expr S)) : Prop :=
…

    Mentions: OAI.PureTypeSystem.ContextTower, OAI.PureTypeSystem.Expr

  12. structure OAI.PureTypeSystem.Candidates.IsCandidate line 81
  13. theorem OAI.PureTypeSystem.Candidates.top_candidate line 86
  14. def OAI.PureTypeSystem.Candidates.Meet line 93

    Source documentation

    The bounded intersection makes the empty meet the typed top.

    def Meet (Ω : ContextTower P) (T : Expr S) (Cs : Set (Set (Expr S))) : Set (Expr S) :=
…

    Mentions: OAI.PureTypeSystem.ContextTower, OAI.PureTypeSystem.Expr

  15. theorem OAI.PureTypeSystem.Candidates.meet_candidate line 96
  16. def OAI.PureTypeSystem.Candidates.Bottom line 106
  17. theorem OAI.PureTypeSystem.Candidates.bottom_candidate line 109
  18. theorem OAI.PureTypeSystem.Candidates.bottom_le line 112
  19. def OAI.PureTypeSystem.Candidates.ProductTest line 116

    Source documentation

    Arbitrary indexed product tests.

    def ProductTest (Ω : ContextTower P) (D E : Expr S) (A : Set (Expr S))
    (Cs : Expr S → Set (Set (Expr S))) : Set (Expr S) :=
…

    Mentions: OAI.PureTypeSystem.ContextTower, OAI.PureTypeSystem.Expr

  20. theorem OAI.PureTypeSystem.Candidates.productTest_candidate line 120
  21. abbrev OAI.PureTypeSystem.Candidates.Candidate line 163
  22. instance OAI.PureTypeSystem.Candidates.(instance at line 165) line 165
  23. instance OAI.PureTypeSystem.Candidates.(instance at line 170) line 170
  24. def OAI.PureTypeSystem.Candidates.SignedCandidate line 181

    Source documentation

    Changing coordinate order changes no candidate sets.

    def SignedCandidate (b : Bool) : Type u := if b then (Candidate Ω T)ᵒᵈ else Candidate Ω T

    Mentions: OAI.PureTypeSystem.Candidates.Candidate

  25. instance OAI.PureTypeSystem.Candidates.(instance at line 183) line 183
  26. def OAI.PureTypeSystem.Candidates.SignedCandidate.set line 191
  27. def OAI.PureTypeSystem.Candidates.SignedCandidate.wrap line 194
  28. theorem OAI.PureTypeSystem.Candidates.SignedCandidate.set_wrap line 197
  29. theorem OAI.PureTypeSystem.Candidates.SignedCandidate.candidate line 200
  30. theorem OAI.PureTypeSystem.Candidates.SignedCandidate.order line 203
  31. theorem OAI.PureTypeSystem.Candidates.SignedCandidate.ext line 207