ranjitjhala

// Run at: http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1427132944.hs

module FizzBuzz where

---------------------------------------------------------------
-- | Implementation: Top level
---------------------------------------------------------------

main      :: IO ()
main      = mapM_ (putStrLn . say) (take 100 $ nums 0)

david-christiansen

module NatInd

import Language.Reflection.Elab
import Language.Reflection.Utils

%default total

trivial : Elab ()
trivial = do compute
             g <- snd <$> getGoal

metanet

import java.io.File
import java.lang.Math.{pow, sqrt}

import scala.annotation.tailrec
import scala.util.Random

case class Point(x: Double, y: Double, z: Double) {
  def distanceTo(that: Point) = sqrt(pow(this.x - that.x, 2) + pow(this.y - that.y, 2) + pow(this.z - that.z, 2))

  def sum(that: Point) = Point(this.x + that.x, this.y + that.y, this.z + that.z)

biboudis

2016

1. Sixth Summer School on Formal Techniques / 22-27 May
2. Twelfth International Summer School on Advanced Computer Architecture and Compilation for High-Performance and Embedded Systems / 10-16 July 2016
3. Oregon Programming Languages Summer School / 20 June-2 July 2016
4. The 6th Halmstad Summer School on Testing / 13-16 June, 2016
5. Second International Summer School on Behavioural Types / 27 June-1 July 2016
6. Virtual Machines Summer School 2016 / 31 May - 3 June 2016
7. ECOOP 2016 Summer School

2015

patik

Squashing Git Commits

The easy and flexible way

This method avoids merge conflicts if you have periodically pulled master into your branch. It also gives you the opportunity to squash into more than 1 commit, or to re-arrange your code into completely different commits (e.g. if you ended up working on three different features but the commits were not consecutive).

Note: You cannot use this method if you intend to open a pull request to merge your feature branch. This method requires committing directly to master.

Switch to the master branch and make sure you are up to date:

david-christiansen

import Language.Reflection.Elab

namespace Tactics

  ||| Restrict a polymorphic type to () for contexts where it doesn't
  ||| matter. This is nice for sticking `debug` in a context where
  ||| Idris can't solve the type.
  simple : {m : Type -> Type} -> m () -> m ()
  simple x = x

biboudis

(* http://fssnip.net/sE in BER MetaOCaml *)

open Runcode;;

let rec fix : (('a -> 'b) -> ('a -> 'b)) -> 'a -> 'b = fun f x ->
  f (fix f) x;;

let fix' : (('a -> 'b) code -> ('a -> 'b) code) -> ('a -> 'b) code = fun f ->
  .< fun x -> let rec loop x = (fun f' -> .~(f .<f'>.) ) loop x in
	      loop x >.;;

puffnfresh

module Compose where

open import Level
open import Function
open import Relation.Binary.PropositionalEquality

record Functor {α} (T : Set α → Set α) : Set (suc α) where
  field
    map : ∀ {A B : Set α} → (A → B) → T A → T B
    identity : ∀ {A : Set α} → map id ≡ id {A = T A}

goldfirere

{-# LANGUAGE TypeOperators, TypeFamilies, TypeApplications,
             ExplicitForAll, ScopedTypeVariables, GADTs, TypeFamilyDependencies,
             TypeInType, ConstraintKinds, UndecidableInstances,
             FlexibleInstances, MultiParamTypeClasses, FunctionalDependencies,
             FlexibleContexts, StandaloneDeriving, InstanceSigs  #-}

module Basics where

import Data.Type.Bool
import Data.Type.Equality

DmitrySoshnikov

/**
 * S-expression parser
 *
 * Recursive descent parser of a simplified sub-set of s-expressions.
 * 
 * NOTE: the format of the programs is used in the "Essentials of interpretation"
 * course: https://github.com/DmitrySoshnikov/Essentials-of-interpretation
 *
 * Grammar:
 *