mgttlinger

#! /usr/bin/env bash

for f in "$@"
do
   pandoc --to=markdown "$f" -o "$f.md"
done

if [ $# -eq 3 ];
then
  emacs -q --eval "(require 'ediff)" --eval "(ediff-files3 \"$1.md\" \"$2.md\" \"$3.md\")"

mgttlinger

{ nixpkgs ? import <nixpkgs> {} }:

nixpkgs.pkgs.callPackage ./minetime.nix {}

mgttlinger

Program Fixpoint rule_transform `{UInverse opu} `{BInverse opb} (p : pro) (free_nominals : Stream nat) (ed : eqn) {measure (complexity p ed)} : EnvT failure (Stream nat) (list eqn) :=
  if orb (is_alpha p ed) (is_beta p ed) then (free_nominals, succ: ([ed])) else
    let av := ed.(a) in
    let bv := ed.(b) in
    match (av, bv, (bmf_pure_in p av, bmf_pure_in p bv)) with
    | (b_conj a1 a2, o, (false, _)) | (o, b_conj a1 a2, (_, false)) => (* /\ rule *)
                                      recurse free_nominals (rule_transform p) [{|a := a1; b := o|}; {|a := a2; b := o|}]
    | (b_negnom x, b_diab o a1 a2, (_, false)) | (b_diab o a1 a2, b_negnom x, (false, _)) => (* binary dia rule *)
                                                 let (n1, n2) := (inr (free_nominals 0) : nom + nat, inr (free_nominals 1)) in (* if the type in there is not explicitly annotated coq inferrs something else which causes a universe inconsistency in the end *)
                                                 fmap (fun r => {|a :=

mgttlinger

module Polyadic

import Data.Vect

parameters (o : Nat -> Type)
  mutual 
    data MT : Nat -> Type where
      Pf : novar f = true -> MT 0
      Iota1 : MT 1
      Iota2 : MT 2

mgttlinger

Module MatchContext.
  Inductive D :=
  | d_a : D
  | d_b : D -> D -> D.
  Fixpoint cmpl d := match d with
                     | d_a => 1
                     | d_b x x0 => S (cmpl x + cmpl x0)
                     end.
  Record T d := {a : d; b : d}.
  Import ListNotations.

mgttlinger

data RT a = N a [RT a] deriving (Show)
no a ns = N a ns
lea a = N a []

sz (N _ cs) = length cs

l (N a cs) = foldl (\accu b -> b) a (l <$> cs) 

slast l = if length l > 0 then Just (last l) else Nothing

mgttlinger

Require Import Vectors.Vector.


Section CT.
  Context {F : Type -> Type}.
  Record Functor__Dict := {
                           fmap__ {a b} : (a -> b) -> F a -> F b;
                           fmap_id__ {t} : forall ft, fmap__ (fun a : t => a) ft = ft;
                           fmap_fusion__ {a b c} : forall (f : a -> b) (g : b -> c) fa, fmap__ g (fmap__ f fa) = fmap__ (fun e => g (f e)) fa
                         }.

mgttlinger

Require Import Vectors.Vector.

Import VectorNotations.
Section CT.
  Context {F : Type -> Type}.
  Record Functor__Dict := {
                           fmap__ {a b} : (a -> b) -> F a -> F b;
                           fmap_id__ {t} : forall ft, fmap__ (fun a : t => a) ft = ft;
                           fmap_fusion__ {a b c} : forall (f : a -> b) (g : b -> c) fa, fmap__ g (fmap__ f fa) = fmap__ (fun e => g (f e)) fa
                         }.

mgttlinger

Section CT.
  Context {F : Set -> Set}.
  Class Functor := { fmap {a b : Set} : (a -> b) -> F a -> F b;
                     fmap_id {t : Set} : forall ft, fmap (fun a : t => a) ft = ft;
                     fmap_fusion {a b c : Set} : forall (f : a -> b) (g : b -> c) fa, fmap g (fmap f fa) = fmap (fun e => g (f e)) fa 
                   }.

  Class Pure `{Functor} := { pure {t : Set} : t -> F t }.
  Class Applicative `{Pure} := { zip {a b : Set} : F a -> F b -> F (a * b)%type;
                                 ap {a b : Set} : F (a -> b) -> F a -> F b := fun ff fa => fmap (fun t => match t with (f, e) => f e end) (zip ff fa);

mgttlinger

Keybase proof

I hereby claim:

• I am mgttlinger on github.
• I am mgttlinger (https://keybase.io/mgttlinger) on keybase.
• I have a public key ASDg_8KGStC1qz4to97HYutUaVq-tWcMHYf98CR5HVL2aQo

To claim this, I am signing this object: