Commit 2023-11-05 21:52 37eb0688

View on Github →

feat: a solution to if-normalization (#8035)

  • feat: a solution to if-normalization
  • lint
  • import all
  • duplicated names
  • Update Archive/Examples/IfNormalization/Statement.lean
  • resist the temptation to let aesop specify the data
  • typo in doc-string
  • workaround
  • fix
  • fix
  • fix

Estimated changes

added theorem IfExpr.eval_ite_ite
added theorem IfExpr.eval_ite_lit
added theorem IfExpr.eval_ite_var
added theorem IfExpr.eval_lit
added theorem IfExpr.eval_var
added def IfExpr.normSize
added def IfExpr.normalize
added def IfExpr.disjoint
added def IfExpr.eval
added def IfExpr.vars
added inductive IfExpr
added def IfNormalization
added def List.disjoint
added theorem IfExpr.eval_ite_ite'
added def IfExpr.normSize'