OAI/Computability/TypeSystem/Basic.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Full annotated PTS syntax, modulo alpha-renaming via de Bruijn indices. Contexts are stored newest-first, each declaration in its prefix context. No functionality assumptions on axioms or product rules.

  1. inductive OAI.PureTypeSystem.Expr line 15

    Also declared: ComparatorChallenges/TypeSystemNormalization.lean:15 (same declaration text).

  2. def OAI.PureTypeSystem.Expr.liftRen line 27

    Also declared: ComparatorChallenges/TypeSystemNormalization.lean:27 (same declaration text).

  3. def OAI.PureTypeSystem.Expr.rename line 31

    Also declared: ComparatorChallenges/TypeSystemNormalization.lean:31 (same declaration text).

  4. def OAI.PureTypeSystem.Expr.liftSub line 38

    Also declared: ComparatorChallenges/TypeSystemNormalization.lean:38 (same declaration text).

  5. def OAI.PureTypeSystem.Expr.subst line 42

    Also declared: ComparatorChallenges/TypeSystemNormalization.lean:42 (same declaration text).

  6. def OAI.PureTypeSystem.Expr.single line 49

    Also declared: ComparatorChallenges/TypeSystemNormalization.lean:49 (same declaration text).

  7. def OAI.PureTypeSystem.Expr.instantiate line 53

    Also declared: ComparatorChallenges/TypeSystemNormalization.lean:53 (same declaration text).

  8. structure OAI.PureTypeSystem.Specification line 57

    Also declared: ComparatorChallenges/TypeSystemNormalization.lean:57 (same declaration text).

  9. inductive OAI.PureTypeSystem.Beta line 61

    Also declared: ComparatorChallenges/TypeSystemNormalization.lean:61 (same declaration text).

  10. def OAI.PureTypeSystem.Converts line 70

    Also declared: ComparatorChallenges/TypeSystemNormalization.lean:70 (same declaration text).

  11. def OAI.PureTypeSystem.Normal line 72

    Also declared: ComparatorChallenges/TypeSystemNormalization.lean:72 (same declaration text).

  12. def OAI.PureTypeSystem.WeaklyNormalizing line 74

    Also declared: ComparatorChallenges/TypeSystemNormalization.lean:74 (same declaration text).

  13. def OAI.PureTypeSystem.StronglyNormalizing line 79

    Source documentation

    Accessibility for the converse of reduction: strong normalization, including reductions in all type annotations.

    Also declared: ComparatorChallenges/TypeSystemNormalization.lean:79 (same declaration text).

    def StronglyNormalizing {S : Type u} (M : Expr S) : Prop :=
…

    Mentions: OAI.PureTypeSystem.Expr

  14. inductive OAI.PureTypeSystem.HasType line 82

    Also declared: ComparatorChallenges/TypeSystemNormalization.lean:82 (same declaration text).

  15. inductive OAI.PureTypeSystem.ValidContext line 100

    Also declared: ComparatorChallenges/TypeSystemNormalization.lean:100 (same declaration text).

  16. def OAI.PureTypeSystem.Legal line 105

    Also declared: ComparatorChallenges/TypeSystemNormalization.lean:105 (same declaration text).

  17. def OAI.PureTypeSystem.SystemWeaklyNormalizing line 108

    Also declared: ComparatorChallenges/TypeSystemNormalization.lean:108 (same declaration text).

  18. def OAI.PureTypeSystem.SystemStronglyNormalizing line 111

    Also declared: ComparatorChallenges/TypeSystemNormalization.lean:111 (same declaration text).

  19. theorem OAI.PureTypeSystem.HasType.valid line 119
  20. theorem OAI.PureTypeSystem.Expr.liftRen_zero line 135
  21. theorem OAI.PureTypeSystem.Expr.liftRen_succ line 136
  22. theorem OAI.PureTypeSystem.Expr.liftRen_id line 139
  23. theorem OAI.PureTypeSystem.Expr.liftRen_comp line 143
  24. theorem OAI.PureTypeSystem.Expr.rename_id line 147
  25. theorem OAI.PureTypeSystem.Expr.rename_comp line 155
  26. theorem OAI.PureTypeSystem.Expr.liftSub_zero line 164
  27. theorem OAI.PureTypeSystem.Expr.liftSub_succ line 165
  28. theorem OAI.PureTypeSystem.Expr.liftSub_var line 168
  29. theorem OAI.PureTypeSystem.Expr.subst_var line 172
  30. theorem OAI.PureTypeSystem.Expr.subst_rename line 180
  31. theorem OAI.PureTypeSystem.Expr.rename_subst line 194
  32. theorem OAI.PureTypeSystem.Expr.subst_subst line 213
  33. theorem OAI.PureTypeSystem.Expr.instantiate_rename line 232
  34. theorem OAI.PureTypeSystem.Expr.instantiate_subst line 239
  35. theorem OAI.PureTypeSystem.Beta.rename line 256
  36. theorem OAI.PureTypeSystem.Beta.subst line 268