schrodibear

theory Bug
  imports HOL.Argo HOL.Metis ― ‹A minimalistic import for faster propagation of changes in Argo›
begin

lemma
  "¬ subseteq
     (Field (image (apsnd Container) (rel (upd h_ent (Object ob) (single (pair c n))))))
     s'_entities ⟶
   member 
     (w

schrodibear

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}

module Common where
  data Empty
  data Nonempty

  type family a + b where

schrodibear

type _ wit = ..

type (_, _, 'e) app = ..

let (%) f g x = f (g x)

module Freer : sig
  type ('a, 'e, 'h) t = private
    | Pure of 'a
    | Impure : 't wit * ('b, 't, 'e) app * ('b -> ('a, 'e, 'h) t) -> ('a, 'e, 'h) t