#![deny(missing_docs)]
#![deny(dead_code)]
#![feature(marker_trait_attr)]
#![allow(incomplete_features)]
#![allow(clippy::type_complexity)]
use std::rc::Rc;
use Either::*;
pub mod and;
#[cfg(feature = "avatar_extensions")]
pub mod avatar_extensions;
pub mod imply;
pub mod eq;
pub mod not;
pub mod or;
pub mod path_semantics;
pub mod nat;
pub mod quality;
pub mod quality_traits;
pub mod qubit;
pub mod queenity;
pub mod univalence;
#[cfg(feature = "quantify")]
pub mod quantify;
pub mod existence;
pub mod con_qubit;
pub mod hooo;
pub mod hooo_traits;
pub mod modal;
pub mod ava_modal;
pub mod mid;
pub mod fun;
#[derive(Copy, Clone)]
pub struct True;
#[derive(Copy, Clone)]
pub enum False {}
#[derive(Copy, Clone)]
pub enum Either<T, U> {
Left(T),
Right(U),
}
pub type And<T, U> = (T, U);
pub type Dneg<T> = Imply<Not<Not<T>>, T>;
pub type Eq<T, U> = And<Imply<T, U>, Imply<U, T>>;
pub type Iff<T, U> = Eq<T, U>;
pub type Imply<T, U> = Rc<dyn Fn(T) -> U>;
pub type ExcM<T> = Or<T, Not<T>>;
pub type Not<T> = Imply<T, False>;
pub type Or<T, U> = Either<T, U>;
pub trait Prop: 'static + Sized + Clone {
fn double_neg(self) -> Dneg<Self> {self.map_any()}
fn map_any<T>(self) -> Imply<T, Self> {Rc::new(move |_| self.clone())}
fn nnexcm() -> Not<Not<ExcM<Self>>> {
Rc::new(move |nexcm| {
let nexcm2 = nexcm.clone();
let f: Not<Self> = Rc::new(move |a| nexcm2(Left(a)));
let g: Not<Not<Self>> = Rc::new(move |na| nexcm(Right(na)));
g(f)
})
}
}
impl<T: 'static + Sized + Clone> Prop for T {}
pub trait Decidable: Prop {
fn decide() -> ExcM<Self>;
}
impl Decidable for True {
fn decide() -> ExcM<True> {Left(True)}
}
impl Decidable for False {
fn decide() -> ExcM<False> {Right(Rc::new(move |x| x))}
}
impl<T, U> Decidable for And<T, U> where T: Decidable, U: Decidable {
fn decide() -> ExcM<Self> {
match (<T as Decidable>::decide(), <U as Decidable>::decide()) {
(Left(a), Left(b)) => Left((a, b)),
(_, Right(b)) => Right(Rc::new(move |(_, x)| b.clone()(x))),
(Right(a), _) => Right(Rc::new(move |(x, _)| a.clone()(x))),
}
}
}
impl<T, U> Decidable for Or<T, U> where T: Decidable, U: Decidable {
fn decide() -> ExcM<Self> {
match (<T as Decidable>::decide(), <U as Decidable>::decide()) {
(Left(a), _) => Left(Left(a)),
(_, Left(b)) => Left(Right(b)),
(Right(a), Right(b)) => Right(Rc::new(move |f| match f {
Left(x) => a.clone()(x),
Right(y) => b.clone()(y),
}))
}
}
}
impl<T, U> Decidable for Imply<T, U> where T: Decidable, U: Decidable {
fn decide() -> ExcM<Self> {
match (<T as Decidable>::decide(), <U as Decidable>::decide()) {
(_, Left(b)) => Left(b.map_any()),
(Left(a), Right(b)) =>
Right(Rc::new(move |f| b.clone()(f(a.clone())))),
(Right(a), _) => {
let g: Imply<Not<U>, Not<T>> = a.map_any();
Left(imply::rev_modus_tollens(g))
}
}
}
}
pub trait DProp: Decidable {}
impl<T: Decidable> DProp for T {}