jfdm

module Domains

allLTE : List Int -> Bool
allLTE Nil        = True
allLTE (x::Nil)   = True
allLTE (x::y::xs) = x < y && allLTE (y::xs)

data VRange : Int -> Int -> Bool -> Type where
  MkVRange  : VRange x y (x <= y)

jfdm

module FoobarE

import Effects
import Effect.State
import Effect.StdIO

namespace Lib
  MyLib : Type -> Type
  MyLib rTy = Eff rTy ['libstate ::: STATE (List Nat), STDIO]

jfdm

-- --------------------------------------------------------------- [ Nines.idr ]
-- Module    : Nines.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : GPL v3
--             see http://choosealicense.com/licenses/gpl-3.0/
-- --------------------------------------------------------------------- [ EOH ]

||| Example of using Dependent Types to implement 'Types as (Abstract)
||| Interpretations'.
|||

jfdm

-- ---------------------------------------------------------------- [ Foos.idr ]
-- Module    : Foos.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : GPL v3
--             see http://choosealicense.com/licenses/gpl-3.0/
-- --------------------------------------------------------------------- [ EOH ]

||| Example of Embedded Domain Specific Type Systems for Declarative EDSLs
|||
||| This example represents the `FooExpr` language, this is a

jfdm

||| The Knock Knock Protocol.
module Knock

import Effects
import Effect.Default
import Effect.StdIO
import Effect.Msg

import System.Protocol

jfdm

%YAML 1.2
%IPKG 0.9.15
---
name: mypackage
version: 0.9.1.2
stability:
synopsis: I am text.
license:
  value: BSD3
  file: LICENSE

jfdm

Keybase proof

I hereby claim:

• I am jfdm on github.
• I am jfdm (https://keybase.io/jfdm) on keybase.
• I have a public key whose fingerprint is F11A C039 D9A1 B71F 7A89 04AE 4955 32C7 14DA 35F2

To claim this, I am signing this object:

jfdm

\documentclass[pdftex, 12pt, a4paper, british, final]{article}

\usepackage[l2tabu,orthodox]{nag}
\usepackage{fixltx2e}
\usepackage{babel}
\usepackage[strict=true]{csquotes}
\usepackage{isodate}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage[protrusion=true, expansion=true]{microtype}

jfdm

;; ott-mode.el -- A Derived mode for writing OTT files
;;
;;; DESCRIPTION
;;
;; A derived mode to highlight OTT input files.
;;
;;; INSTALLATION
;;
;; 1. Place ott-mode.el in your .emacs.d directory
;; 2. Ensure that .emacs.d is on your load path.

jfdm

/** \mainpage
 *
 * __NaCl__ (pronounced _salt_) is a new easy-to-use high-speed
 * software library for network communication, encryption, decryption,
 * signatures, etc. NaCl's goal is to provide all of the core
 * operations needed to build higher-level cryptographic tools.
 *
 * __Sodium__ is a portable, cross-compilable, installable,
 * packageable, API-compatible version of NaCl.
 *