Register
📁 Source: Mathlib/Tactic/Attr/Register.lean
Statistics
Parser.Attr
Definitions
| Name | Category | Theorems |
|---|---|---|
enat_to_nat_coe 📖 | CompOp | — |
enat_to_nat_coe_proc 📖 | CompOp | — |
enat_to_nat_top 📖 | CompOp | — |
enat_to_nat_top_proc 📖 | CompOp | — |
fin_omega 📖 | CompOp | — |
fin_omega_proc 📖 | CompOp | — |
functor_norm 📖 | CompOp | — |
functor_norm_proc 📖 | CompOp | — |
ghost_simps 📖 | CompOp | — |
ghost_simps_proc 📖 | CompOp | — |
integral_simps 📖 | CompOp | — |
integral_simps_proc 📖 | CompOp | — |
is_poly 📖 | CompOp | — |
mfld_simps 📖 | CompOp | — |
mfld_simps_proc 📖 | CompOp | — |
mon_tauto 📖 | CompOp | — |
mon_tauto_proc 📖 | CompOp | — |
monad_norm 📖 | CompOp | — |
monad_norm_proc 📖 | CompOp | — |
nontriviality_proc 📖 | CompOp | — |
parity_simps 📖 | CompOp | — |
parity_simps_proc 📖 | CompOp | — |
pnat_to_nat_coe 📖 | CompOp | — |
pnat_to_nat_coe_proc 📖 | CompOp | — |
qify_simps 📖 | CompOp | — |
qify_simps_proc 📖 | CompOp | — |
rclike_simps 📖 | CompOp | — |
rclike_simps_proc 📖 | CompOp | — |
rify_simps 📖 | CompOp | — |
rify_simps_proc 📖 | CompOp | — |
typevec 📖 | CompOp | — |
typevec_proc 📖 | CompOp | — |
zify_simps 📖 | CompOp | — |
zify_simps_proc 📖 | CompOp | — |
---