silly: a trio from https://penrose.ink

.dsl

type Set
type Point
type Map

constructor Singleton : Point p -> Set

function Intersection : Set a * Set b -> Set
function Union : Set a * Set b -> Set
function Subtraction : Set a * Set b -> Set
function CartesianProduct : Set a * Set b -> Set
function Difference : Set a * Set b -> Set
function Subset : Set a * Set b -> Set
function AddPoint : Point p * Set s1 -> Set

predicate Not : Prop p1
predicate From : Map f * Set domain * Set codomain
predicate Empty : Set s
predicate Intersecting : Set s1 * Set s2
predicate IsSubset : Set s1 * Set s2
predicate PointIn : Set s * Point p
predicate In : Point p * Set s
predicate Injection : Map m
predicate Surjection : Map m
predicate Bijection : Map m
predicate PairIn : Point * Point * Map

notation "A ⊂ B" ~ "IsSubset(A, B)"
notation "p ∈ A" ~ "PointIn(A, p)"
notation "p ∉ A" ~ "PointNotIn(A, p)"
notation "A ∩ B = ∅" ~ "Not(Intersecting(A, B))"
notation "f: A -> B" ~ "Map f; From(f, A, B)"

.sty

Set x {
    x.shape = Circle {
        strokeWidth : 0.
    }

    x.shading = Image {
        center : x.shape.center 
        w : x.shape.r * 2.0
        h : x.shape.r * 2.0
        path : "shading.svg"
    }

    x.shadow = Image {
        path : "shadow.svg"
        w : x.shape.r * 2.15
        h : x.shape.r * 2.22
        center : (x.shape.center[0] + 0.03 * x.shading.w, x.shape.center[1] - 0.051 * x.shading.h)
    }

    x.text = Text {
        string : x.label
        color: rgba(1.0, 1.0, 1.0, 1.0)
        w: 0.5 * x.shape.r
        h: 0.5 * x.shape.r
    }

    ensure contains(x.shape, x.text)
    ensure minSize(x.shape)
    ensure maxSize(x.shape)
    encourage sameCenter(x.text, x.shape)

    x.shape below x.text
    x.shading below x.shape
    x.shadow below x.shading
}

forall Set x; Set y
where IsSubset(x, y) {
    ensure smallerThan(x.shape, y.shape)
    ensure outsideOf(y.text, x.shape)
    ensure contains(y.shape, x.shape, 5.0)
    x.shape above y.shape
    y.text below x.shape
    x.shadow above y.shape
}

Set x; Set y
where Not(Intersecting(x, y)) {
    ensure disjoint(x.shape, y.shape)
}

Set x; Set y
where Intersecting(x, y) {
    ensure overlapping(x.shape, y.shape)
    ensure outsideOf(y.text, x.shape)
    ensure outsideOf(x.text, y.shape)
}

.sub

Set A, B, C, D, E, F, G

IsSubset(B, A)
IsSubset(C, A)
IsSubset(D, B)
IsSubset(E, B)
IsSubset(F, C)
IsSubset(G, C)

Not(Intersecting(E, D))
Not(Intersecting(F, G))
Not(Intersecting(B, C))

AutoLabel All

metadata.json

{"authorship":{"madeBy":"maxkrieger","name":"silly","avatar":"https://avatars.githubusercontent.com/u/2660634?v=4"}}