Macros§
- rules 🔒
Functions§
- addition
- all_
rule_ extractors - all_
symbol_ extractors - any
- apply
- arrow_
for - bind_in
- binl
- binr
- conj
- conjunction
- division
- exponentiation
- hoas_
lpa - implicit
- inhab
- inhabitable
- intersection
- judgment
- lambda
- leq
- letrule
- logarithm
- map
- max
- multiplication
- numcomplex
- numint
- numnat
- numnegint
- numnegrat
- numnegreal
- numnonzeroint
- numnonzerorat
- numnonzeroreal
- numposnat
- numposrat
- numposreal
- numrat
- numreal
- of_type
- pi
- prenex
- prop
- pwconj
- reorder
- subtp
- subtraction
- univ
- universe