abstract type Prop end

abstract type Â¬{A} <: Prop end
abstract type âˆ¨{A, B} <: Prop end
abstract type âˆ§{A, B} <: Prop end
abstract type â†’{A, B} <: Prop end
abstract type â†”{A, B} <: Prop end

abstract type âŠ¤ <: Prop end
abstract type âŠ¥ <: Prop end

abstract type ð�’« <: Prop end

macro variable(A) :(abstract type $A <: ð�’« end) end

@variable P; @variable Q; @variable R

Â¬(::Type{A}) where {A <: Prop} = Â¬{A}
âˆ¨(::Type{A}, ::Type{B}) where {A <: Prop, B <: Prop} = âˆ¨{A, B}
âˆ§(::Type{A}, ::Type{B}) where {A <: Prop, B <: Prop} = âˆ§{A, B}
â†’(::Type{A}, ::Type{B}) where {A <: Prop, B <: Prop} = â†’{A, B}
â†”(::Type{A}, ::Type{B}) where {A <: Prop, B <: Prop} = â†’{A, B}

Base.show(io::IO, ::Type{Â¬{A}}) where {A <: Prop} = print(io, "Â¬$A")
Base.show(io::IO, ::Type{âˆ¨{A, B}}) where {A <: Prop, B <: Prop} = print(io, "($A âˆ¨ $B)")
Base.show(io::IO, ::Type{âˆ§{A, B}}) where {A <: Prop, B <: Prop} = print(io, "($A âˆ§ $B)")
Base.show(io::IO, ::Type{â†’{A, B}}) where {A <: Prop, B <: Prop} = print(io, "($A â†’ $B)")
Base.show(io::IO, ::Type{â†”{A, B}}) where {A <: Prop, B <: Prop} = print(io, "($A â†” $B)")

rewrite(::Type{Â¬{A}}) where {A <: Prop} = rewrite(A â†’ âŠ¥)
rewrite(::Type{âˆ¨{A, B}}) where {A <: Prop, B <: Prop} = rewrite(Â¬A â†’ B)
rewrite(::Type{âˆ§{A, B}}) where {A <: Prop, B <: Prop} = rewrite(Â¬(A â†’ Â¬B))
#rewrite(::Type{â†”{A, B}}) where {A <: Prop, B <: Prop} = rewrite(((A â†’ B) âˆ§ (B â†’ A)))

rewrite(::Type{â†’{A, âŠ¤}}) where {A <: Prop} = âŠ¤
rewrite(::Type{â†’{âŠ¥, A}}) where {A <: Prop} = âŠ¤
rewrite(::Type{â†’{âŠ¤, âŠ¥}}) = âŠ¥


rewrite(::Type{â†’{A, B}}) where {A <: Prop, B <: Prop} = â†’{rewrite(A), rewrite(B)}

rewrite(::Type{âŠ¤}) = âŠ¤
rewrite(::Type{âŠ¥}) = âŠ¥
rewrite(::Type{A}) where {A <: ð�’«} = A

macro assign(A, b) :(rewrite(::Type{$A}) = $b) end
