OAI/Computability/TypeSystem/Substitution.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PureTypeSystem.Expr.compSub line 9
2. theorem OAI.PureTypeSystem.Expr.subst_compSub line 10
3. theorem OAI.PureTypeSystem.Expr.lift_comp_cons line 12
4. theorem OAI.PureTypeSystem.Expr.raise_subst_cons line 17
5. theorem OAI.PureTypeSystem.ObservationValues.SubstitutionGuard.lift line 27
6. def OAI.PureTypeSystem.ObservationValues.GoodReplacement line 41

   Source documentation

   Goodness assumptions on the values grafted at declarations.

   def GoodReplacement {Γ Δ : List (Expr S)} {σ : Nat → Expr S}
       (ts : TypingTree.StoredSubstitution P Γ Δ σ) (ξ : Nat → Expr S) : Prop :=
   …

   Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.TypingTree.StoredSubstitution

7. theorem OAI.PureTypeSystem.ObservationValues.goodReplacement_lift line 46
8. theorem OAI.PureTypeSystem.ObservationValues.neutral_readGood line 81
9. theorem OAI.PureTypeSystem.ObservationValues.PreResult.sort_val_retarget line 109
10. theorem OAI.PureTypeSystem.ObservationValues.PreResult.lookup_val_retarget line 118
11. theorem OAI.PureTypeSystem.ObservationValues.PreResult.abstractionAction_retarget line 127
12. theorem OAI.PureTypeSystem.ObservationValues.PreResult.abstraction_val_retarget line 159
13. theorem OAI.PureTypeSystem.ObservationValues.PreResult.product_val_retarget line 172
14. theorem OAI.PureTypeSystem.ObservationValues.PreResult.application_val_retarget line 188
15. theorem OAI.PureTypeSystem.ObservationValues.preEvaluate_retarget_val line 205
16. theorem OAI.PureTypeSystem.ObservationValues.preEvaluate_retarget_parameter line 219
17. structure OAI.PureTypeSystem.ObservationValues.Environment.Assigned line 228
18. theorem OAI.PureTypeSystem.ObservationValues.Environment.Assigned.raw_eq line 238
19. theorem OAI.PureTypeSystem.ObservationValues.Environment.Assigned.normal_eq line 240
20. theorem OAI.PureTypeSystem.ObservationValues.Environment.Assigned.cons line 244
21. theorem OAI.PureTypeSystem.ObservationValues.preEvaluate_read_outside line 281
22. theorem OAI.PureTypeSystem.ObservationValues.preEvaluate_neutral_read_inactive line 292
23. theorem OAI.PureTypeSystem.ObservationValues.readGood_outside line 315
24. abbrev OAI.PureTypeSystem.ObservationValues.ProductGood line 324
25. theorem OAI.PureTypeSystem.ObservationValues.goodness_subst line 330
26. theorem OAI.PureTypeSystem.ObservationValues.baseRead_substitution line 450
27. theorem OAI.PureTypeSystem.ObservationValues.preEvaluate_subst line 485
28. theorem OAI.PureTypeSystem.Expr.comp_single line 610
29. def OAI.PureTypeSystem.TypingTree.StoredSubstitution.single line 616
30. theorem OAI.PureTypeSystem.ObservationValues.goodness_recontext line 638
31. theorem OAI.PureTypeSystem.ObservationValues.single_guard line 671
32. theorem OAI.PureTypeSystem.ObservationValues.single_goodReplacement line 680
33. theorem OAI.PureTypeSystem.ObservationValues.single_assigned line 693