Skip to content

Instantly share code, notes, and snippets.

Avatar

Mikhail Mandrykin schrodibear

View GitHub Profile
View Bug.thy
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
View Common.hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
module Common where
data Empty
data Nonempty
type family a + b where
View freer_file_reader_and_writer.ml
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