googleson78

tauren :: /tmp/liquid » tree
.
├── Crash.hs
└── include
    └── Data
        └── Text.spec

2 directories, 2 files

tauren :: /tmp/liquid » cat Crash.hs

googleson78

    Fusion
      fusion
        Union proofs should simplify FAILED [1]
        internal uses of StateT should simplify
        internal uses of ExceptT should simplify
        `runState . reinterpret` should fuse
        who needs Sematic even?
    Output
      runBatchOutput
        should return nothing at batch size 0

googleson78

-- empty type
data ⊥ : Set where

-- can't prove this so we introduce it as an axiom
postulate
    stab : ∀{A : Set} -> ((A -> ⊥) -> ⊥) -> A

-- if you give me an x of type X and an inhabitant of P x, then I have proof that there exists an inhabitant of P x
data ∃ {X : Set} (P : X -> Set) : Set where
    intro-∃ : ∀(x : X) -> P x -> ∃ P

googleson78

data A = A ()
  deriving Show

a :: A
a = (f a)

f :: A -> A
f (A x) = A ()