OAI/ModelTheory/Choiceless/FullLanguage.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CPTSeparation.FullCPT.bindSlots line 17
  2. def OAI.CPTSeparation.FullCPT.Agrees line 20
  3. lemma OAI.CPTSeparation.FullCPT.agrees_bind line 24
  4. def OAI.CPTSeparation.FullCPT.Term.compile line 38
  5. theorem OAI.CPTSeparation.FullCPT.Term.eval_compile line 61
  6. def OAI.CPTSeparation.FullCPT.Rule.compile line 109
  7. theorem OAI.CPTSeparation.FullCPT.Rule.updates_compile line 117
  8. def OAI.CPTSeparation.FullCPT.Program.accepts line 145
  9. def OAI.CPTSeparation.FullCPT.Program.compile line 149
  10. lemma OAI.CPTSeparation.FullCPT.Program.flag_compile line 156
  11. lemma OAI.CPTSeparation.FullCPT.Program.step_compile line 162
  12. lemma OAI.CPTSeparation.FullCPT.Program.run_compile line 173
  13. lemma OAI.CPTSeparation.FullCPT.Program.active_compile line 183
  14. lemma OAI.CPTSeparation.FullCPT.Program.accepts_compile line 191
  15. def OAI.CPTSeparation.FullCPT.Definable line 199
  16. theorem OAI.CPTSeparation.FullCPT.query_not_definable line 203