basic): Add function.update_apply (#5093)

Commit

5 years ago

chore(logic/function/basic): Add function.update_apply (#5093) This makes it easier to eliminate `dite`s in simple situations when only `ite` is needed.

Author

eric-wieser

Parents

81207e09

mathlib3 6e301c75 - chore(logic/function/basic): Add function.update_apply (#5093)

mathlib3
6e301c75 - chore(logic/function/basic): Add function.update_apply (#5093)