myuon myuon

myuon / Trans.thy

Last active December 16, 2017 05:32 — forked from yksym/Trans.thy

memo: star to list

	theory Trans
	imports Main
	begin
	(* "Lectures on the Curry-Howard Isomorphism" Lemma 1.4.2 *)

	inductive star :: "( 'a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool" for r where
	lift: "r x y ⟹ star r x y" \|
	trans: "star r x y ⟹ star r y z ⟹ star r x z"

	inductive trans_list :: "( 'a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ bool" for r where

myuon / 0_reuse_code.js

Created November 11, 2013 02:05

Here are some things you can do with Gists in GistBox.

	// Use Gists to store code you would like to remember later on
	console.log(window); // log the "window" object to the console

myuon / gist:3726663

Created September 15, 2012 06:46 — forked from ikedaisuke/gist:916931

Rotate a square in Gloss (with key event (DOWN-key))

	module Main where

	-- http://www.f13g.com/%A5%D7%A5%ED%A5%B0%A5%E9%A5%DF%A5%F3%A5%B0/Haskell/GLUT/#content_1_4

	import Graphics.Gloss
	import Graphics.Gloss.Interface.Pure.Game

	data State
	= State { angle :: Float
	, isPositive :: Bool