righ1113

// "zdkRec.pp" load

"zdkSub" :
  random 0.5 > if
    1 +
    "Zun" .
    zdkSub
  else
    "Doko" .
    4 >= if

righ1113

\ s" oop.f" included

require /snap/gforth/15/share/gforth/0.7.9_20201105/objects.fs

object class \ "object" is the parent class
  selector hoge
  selector hoge2
  selector foo
  selector setCr
end-class myCls'

righ1113

\ s" collatz.f" included

: m3p1    ( n -- n' )
    3 * 1 + ;
: choice  ( n b -- n' )
    1 = if m3p1 else 2 / then ; \ 比較対象は消える
: myMod2  ( n -- n n b )
    dup dup 2 mod ;
: collatz ( n -- n a b .. 1 )
    recursive dup 1 = if else myMod2 choice collatz then ;

righ1113

module Rand2 where

-- stack install random
-- stack install list-t
-- stack exec ghci

import Control.Monad.IO.Class ( liftIO )
import ListT                  ( ListT, toList, cons, take )
import System.Random          ( Random(randomIO) )

righ1113

{-# LANGUAGE Arrows #-}
module ALoop where

import Control.Arrow ( returnA, ArrowLoop(loop) )


-- loop f b = let (c,d) = f (b,d) in c
fact :: Int -> Int
fact = loop $ \(x, f) -> (f x, \n -> if n == 0 then 1 else n * f (n - 1))

righ1113

Require Import Arith. (* lt_wf *)
(* Require Import Omega. *)

Hypothesis div2 : forall x, x / 2 < x.
Hypothesis mul2 : forall x y z w, x = y / 2 * z + w -> x * 2 = y * z + w * 2.

Theorem erdos2 :
  forall n,
    (exists c x y, 4 * c * x * y = n * (1 + x) + y).
Proof.

righ1113

;; gosh> (gauche-version)
;; "0.9.5"
;; egison.scm は https://github.com/egison/egison-scheme/blob/master/egison.scm
;; から取得し、モジュール化しておく
;; > (add-load-path "./send")
;; > (use send)
;; リロード時 > (reload 'send)


;; モジュールのインタフェースの定義

righ1113

-- $ chcp 65001
-- $ idris
-- > :l Comm
module Comm

%default total

comm : (x, y : Nat) -> x + y = y + x
comm Z     Z     = Refl
comm (S x) Z     = rewrite plusZeroRightNeutral x in Refl

righ1113

E:\me\Egison\quine>egison quine.egi
main args := let s := "main args := let s := Z in print (S.replace (pack [upperCase 'z']) (show s) s)" in print (S.replace (pack [upperCase 'z']) (show s) s)

E:\me\Egison\quine>type quine.egi
main args := let s := "main args := let s := Z in print (S.replace (pack [upperCase 'z']) (show s) s)" in print (S.replace (pack [upperCase 'z']) (show s) s)


E:\me\Egison\quine>egison quine2.egi
main args :=
  print (S.append s (show s)) where

righ1113

-- Egison Version >= 3.10.0
-- $ egison -N
-- > loadFile "sort.egins"



--
-- Utils
--