ksk

(* Zagier's one-sentence proof for the two-square theorem in Coq (SSReflect) *)
(* - D. Zagier, "A One-Sentence Proof That Every Prime p \equiv 1 (\mod 4) Is a Sum of Two Squares", 
     The American Mathematical Monthly, Vol. 97, No. 2 (Feb., 1990), p. 144 *)

Set Implicit Arguments. Unset Strict Implicit.
From mathcomp Require Import all_ssreflect.

Lemma odd_fixedpoints {X:eqType} (f:X->X) (D:seq X):
  uniq D -> (forall x, x \in D -> (f x \in D) && (f (f x) == x)) ->
  odd (size D) <-> odd (count [pred x | f x == x] D).

egisatoshi

concat (matchAll (["akira", "susumu", "tamotsu", "tomo"], ["blue", "green", "red", "white"], [1, 2, 3, 4])
              as (list something, multiset something, multiset something) with
          | ([$x_1, $x_2, $x_3, $x_4], [$y_1, $y_2, $y_3, $y_4], [$z_1, $z_2, $z_3, $z_4])
          -> matchAll [(x_1, y_1, z_1), (x_2, y_2, z_2), (x_3, y_3, z_3), (x_4, y_4, z_4)]
                   as set (eq, eq, eq) with
               | (#"akira", #"blue", !#1) ::
                 (#"susumu", !#"green", !#4) ::
                 (_, #"red", #2) ::
                 (_, #"white", $n) ::
                 (#"tamotsu", _, #(n - 1)) :: _

SekiT

data FizzDataType : Type where
  FizzData : FizzDataType

data BuzzDataType : Type where
  BuzzData : BuzzDataType

data FizzBuzzDataType : Type where
  FizzBuzzData : FizzBuzzDataType

data NatDataType : (n : Nat) -> Type where

kyodaisuu

#!/usr/bin/python
# coding: utf-8
# Print Graham's number
# 
# Just a code for showing definition.
# It causes runtime error of maximum recursion.

def G(n):
    # G function of Graham's number
    if n == 0:

hatsugai

(*
  Tarski's fixed-point theorem on sets (complete lattice)
  Isabelle 2014
*)
theory Tarski imports Main begin

lemma fp1: "mono F ==> F (Inter {X. F X <= X}) <= Inter {X. F X <= X}"
apply(rule subsetI)
apply(rule InterI)
apply(simp)

nyuichi

; -*- mode: scheme;-*-
; Implementation of resolution principle for first-order logic in Egison

(define $unordered-pair
 (lambda [$m]
  (matcher
    {[<pair $ $> [m m] {[[$x $y] {[x y] [y x]}]}]
     [$ [something] {[$tgt {tgt}]}]})))

(define $positive?

WhiteCat6142

bsort=foldr bs []
 where bs x []=[x]
       bs x (y:ys)|x<=y =(x:y:ys)
                  |otherwise =(y:bs x ys)

ekmett

-- http://comonad.com/reader/2018/the-state-comonad/
-- https://www.reddit.com/r/haskell/comments/7oav51/i_made_a_monad_that_i_havent_seen_before_and_i/

{-# language DeriveFunctor #-}

import Control.Comonad
import Data.Semigroup

data Store s a = Store { peek :: s -> a, pos :: s } deriving Functor

cutsea110

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures,
             TypeSynonymInstances,
             FlexibleInstances
#-}
module FixPrime where

import Prelude hiding (Functor(..), map, succ, either)

pair (f, g) x = (f x, g x)

ashiato45

sig Element{}

one sig Group{
	elements: set Element,
	unit: one elements,
	mult: elements -> elements -> one elements,
	inv: elements -> one elements
}

fact NoRedundantElements{