myuon

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

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

myuon

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