List of all items
Structs
- True
- avatar_extensions::AntiMul
- avatar_extensions::Inv
- avatar_extensions::Loop
- nat::NaN
- nat::S
- nat::Z
- path_semantics::LTrue
- path_semantics::POrdProof
- quality::Q
Enums
Traits
- DProp
- Decidable
- Prop
- avatar_extensions::Avatar
- avatar_extensions::Commutative
- avatar_extensions::Contravariant
- avatar_extensions::LoopWitness
- avatar_extensions::NonUniform
- avatar_extensions::Product
- avatar_extensions::Uniform
- nat::Add
- nat::EqNat
- nat::Lt
- nat::Nat
- path_semantics::DLProp
- path_semantics::LProp
- path_semantics::Lookup
- path_semantics::POrd
- path_semantics::SortMax
- path_semantics::SortMin
Functions
- and::assoc
- and::commute
- and::distrib
- and::exc_both
- and::exc_left
- and::exc_right
- and::false_arg
- and::from_de_morgan
- and::from_imply
- and::in_left_arg
- and::in_right_arg
- and::to_de_morgan
- and::to_eq_neg
- and::to_eq_pos
- and::to_imply
- and::true_arg
- avatar_extensions::left_cover_by_proof
- avatar_extensions::right_cover_by_proof
- avatar_extensions::to_loop
- eq::absurd
- eq::assoc
- eq::assoc_eq
- eq::assoc_left
- eq::assoc_right
- eq::commute
- eq::commute_eq
- eq::contra
- eq::double_neg
- eq::imply_to_or
- eq::in_left_arg
- eq::in_right_arg
- eq::inv_triangle
- eq::is_false
- eq::is_true
- eq::modus_tollens
- eq::refl
- eq::rev_modus_tollens
- eq::swap_left
- eq::swap_right
- eq::to_eq_false
- eq::transitivity
- eq::transpose
- eq::triangle
- eq::true_eq
- imply::absurd
- imply::chain
- imply::double_neg
- imply::flip_neg_left
- imply::flip_neg_right
- imply::from_or
- imply::id
- imply::in_left_arg
- imply::in_right_arg
- imply::join
- imply::modus_ponens
- imply::modus_tollens
- imply::reorder_args
- imply::rev_double_neg
- imply::rev_modus_ponens
- imply::rev_modus_tollens
- imply::to_or
- imply::transitivity
- nat::eq
- nat::lt
- not::absurd
- not::double
- not::rev_double
- or::assoc
- or::bound_neg
- or::bound_pos
- or::commute
- or::distrib
- or::from_de_morgan
- or::in_left_arg
- or::in_right_arg
- or::to_de_morgan
- path_semantics::assume
- path_semantics::assume_inc_path_level
- path_semantics::assume_naive
- path_semantics::assume_norm_path_level
- path_semantics::assume_refl
- path_semantics::check_q
- path_semantics::comp
- path_semantics::eq_lev
- path_semantics::lt_lev
- path_semantics::naive_comp
- path_semantics::naive_red_false
- path_semantics::pand_both_eq
- path_semantics::to_naive
- path_semantics::to_pand_fst
- path_semantics::to_pand_snd
- path_semantics::to_por_fst
- path_semantics::to_por_snd
- path_semantics::uniq_ty
- path_semantics::use_pand_both
- path_semantics::xy_norm
- quality::absurd_plato
- quality::commute
- quality::eq_maybe_lift
- quality::excm_plato_refl
- quality::mirror_plato
- quality::self_quality_left
- quality::self_quality_right
- quality::sesh_left
- quality::sesh_plato_absurd
- quality::sesh_right
- quality::to_eq
- quality::transitivity
Typedefs
- And
- Dneg
- Eq
- ExcM
- Iff
- Imply
- Not
- Or
- nat::One
- nat::Three
- nat::Two
- nat::Zero
- path_semantics::Inc
- path_semantics::IncLevel
- path_semantics::LN
- path_semantics::Max
- path_semantics::MaxMax
- path_semantics::MaxMin
- path_semantics::Maxi
- path_semantics::Min
- path_semantics::MinMax
- path_semantics::MinMin
- path_semantics::Mixi
- path_semantics::Normalise
- path_semantics::PAndFst
- path_semantics::PAndSnd
- path_semantics::POrFst
- path_semantics::POrSnd
- path_semantics::PSem
- path_semantics::PSemNaive
- path_semantics::PSemNaiveNorm
- quality::EqQ
- quality::PurePlatonism