jfdm

record Bumpable type where
  constructor B
  bump : type -> type


myIntBumper : Bumpable Int
myIntBumper
  = B (+ 1)

jfdm

// Sadly first class types do not exist in dafny, so we have to copy the Rust Approach of abusing generics.
//
// https://docs.rs/session_types/
//
// https://github.com/NicolasLagaillardie/mpst_rust_github
//
// There must be a better way!
datatype Stop        = ActStop

datatype Send<A,B>   = ActSend(A,B)

jfdm

module AocDay1

import Decidable.Equality
import Data.List.Quantifiers
import Data.Singleton
import Data.String

data Length : Any p xs -> Nat -> Type  where
  Here : Length (Here p)  Z
  There : Length ltr n

jfdm

#!/usr/bin/env cabal
{- cabal:
build-depends: base
             , yaml
             , text
             , bytestring
-}
{-# LANGUAGE DeriveGeneric, OverloadedStrings, DuplicateRecordFields, DeriveAnyClass #-}
module Main where

jfdm

module Flag
import Control.Relation
import Control.WellFounded
import Data.Nat
import Data.DPair
import Data.List
import Data.List.Views

%default total

jfdm

Merging Local Types for Synthesis

This document is a literate Idris2 file that the compiler can understand, and if one uses polymode for eMacs can highlight…

In this document, we outline a proof of Merge For Synthesis for a simple representation of Local type. Merging this into Capable is going to be trifficult!

Preamble

jfdm

module SystemF

import Decidable.Equality

import Data.SnocList.Elem

namespace Kind
  public export
  data Kind : Type
    where ||| Types of Types

jfdm

module Bar

import System
import System.File

import Data.String

namespace Main
  export
  main : IO ()

jfdm

\documentclass{article}

\usepackage{xspace}
% The Magic Sauce.

\usepackage{scrletter}

\makeatletter
\newkomavar[urghhh]{documentTitle}
\setkomavar{documentTitle}{\@title}

jfdm

#!/bin/env bash

test ! -z $1 && set -x # Show commands if first arg is non-zero

mkdir -p build/html

katla_run()
{
    KATLA_EXE=$(which katla)
    test -x KATLA_EXE && echo "Katla not installed"