lean4-htt/library/init/meta
Leonardo de Moura a31f12d8cd chore(library/init/core): revert ite+thunks modification
We don't need it since we marked `ite` as `[macro_inline]`
2018-09-23 19:27:06 -07:00
..
default.lean
format.lean chore(library/init/core): revert ite+thunks modification 2018-09-23 19:27:06 -07:00
interaction_monad.lean
name.lean feat(library/init/core): decidable_eq is a proper class 2018-09-07 16:38:11 -07:00
options.lean
pos.lean feat(library/init/core): decidable_eq is a proper class 2018-09-07 16:38:11 -07:00
ref.lean
tactic.lean chore(library): remove return, we should use pure 2018-09-12 16:51:11 -07:00