yksym

#include <typeinfo>

//g++ -std=gnu++0x jikken.cxx                                                                                                                                  
//g++ -std=c++11 jikken.cxx
template <bool B> void sassert()
{
    int dummy[B ? 1:-1];
    dummy[0] = 0;
}

yksym

{-# LANGUAGE DataKinds, TypeOperators, KindSignatures, TypeFamilies #-}
{-# LANGUAGE UndecidableInstances, FlexibleInstances, FlexibleContexts #-}

module IsFun (
    Proxy
  , isFun
  , cntArgs
) where

import Data.Proxy

yksym

-- ref: https://github.com/idris-lang/Idris-dev/blob/0d3d2d66796b172e9933360aee51993a4abc624d/test/totality006/totality006.idr
import Data.So

antitrue : So False -> a
antitrue Oh impossible

total
eqNat : (n : Nat) -> (m : Nat) -> So (n == m) -> (n = m)
eqNat Z Z Oh = Refl
eqNat (S k) Z um = antitrue um -- なぜここでimpossibleが出来ない？

yksym

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

yksym

theory Ex43 imports Main begin

inductive star :: "( 'a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool" for r where
refl: "star r x x" |
step: "r x y ⟹ star r y z ⟹ star r x z"

thm star.step [where ?z = "y"]


lemma r2star: "r x y ⟹ star r x y"

yksym

{-# LANGUAGE PatternSynonyms, DeriveFunctor, FlexibleContexts, TemplateHaskell, RankNTypes #-}
{-# LANGUAGE GeneralizedNewtypeDeriving, StandaloneDeriving, FlexibleInstances, MultiParamTypeClasses #-}
import Data.Bifunctor (first)
import Control.Monad (forever)
import Control.Monad.Coroutine
import Control.Monad.Coroutine.SuspensionFunctors
import Control.Monad.Trans.Class
import Control.Monad.IO.Class
import Control.Monad.State.Class
import Control.Monad.State.Lazy