OAI/Computability/BinPacking/Arithmetic/NatExpression.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.BinPackingGap.NatExpressionCompiler.Expr line 10
  2. def OAI.BinPackingGap.NatExpressionCompiler.eval line 19
  3. theorem OAI.BinPackingGap.NatExpressionCompiler.eval_constant line 26
  4. theorem OAI.BinPackingGap.NatExpressionCompiler.eval_input line 29
  5. theorem OAI.BinPackingGap.NatExpressionCompiler.eval_add line 32
  6. theorem OAI.BinPackingGap.NatExpressionCompiler.eval_mul line 35
  7. theorem OAI.BinPackingGap.NatExpressionCompiler.eval_monus line 38
  8. def OAI.BinPackingGap.NatExpressionCompiler.Node line 41
  9. instance OAI.BinPackingGap.NatExpressionCompiler.nodeFintype line 48
  10. instance OAI.BinPackingGap.NatExpressionCompiler.nodeDecidableEq line 64
  11. def OAI.BinPackingGap.NatExpressionCompiler.rootBranch line 80
  12. def OAI.BinPackingGap.NatExpressionCompiler.root line 83
  13. theorem OAI.BinPackingGap.NatExpressionCompiler.rootBranch_eq line 90
  14. theorem OAI.BinPackingGap.NatExpressionCompiler.root_constant line 93
  15. theorem OAI.BinPackingGap.NatExpressionCompiler.root_input line 96
  16. theorem OAI.BinPackingGap.NatExpressionCompiler.root_add line 98
  17. theorem OAI.BinPackingGap.NatExpressionCompiler.root_mul line 101
  18. theorem OAI.BinPackingGap.NatExpressionCompiler.root_monus line 104
  19. def OAI.BinPackingGap.NatExpressionCompiler.leftNode line 107
  20. def OAI.BinPackingGap.NatExpressionCompiler.rightNode line 113
  21. theorem OAI.BinPackingGap.NatExpressionCompiler.leftNode_apply line 119
  22. theorem OAI.BinPackingGap.NatExpressionCompiler.rightNode_apply line 122