Skip to content

Instantly share code, notes, and snippets.

Rotsor

Block or report user

Report or block Rotsor

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@Rotsor
Rotsor / strange-monad.agda
Created Jul 9, 2019
A weird tree monad proposed on reddit
View strange-monad.agda
-- a proof of monad laws for a strange monad defined in:
-- https://www.reddit.com/r/haskell/comments/cb1j40/is_there_a_valid_monad_instance_for_binary_trees/etcqsts/
data TREE (a : Set) : Set where
Leaf : a TREE a
Tree : a TREE a TREE a TREE a
distribute : {a} (TREE a) -> (TREE a) -> (TREE a) -> TREE a
distribute l r (Leaf a) = Tree a l r
distribute l r (Tree a cl cr) = Tree a (distribute l r cl) (distribute l r cr)
@Rotsor
Rotsor / fulcrum.lean
Last active May 15, 2018
Fulcrum in lean
View fulcrum.lean
-- Solution for the "Fulcrum" problem from "The Great Theorem Prover Showdown"
-- (https://www.hillelwayne.com/post/theorem-prover-showdown/)
--
-- I am novice with Lean so the verbosity is almost certainly my
-- fault and not that of Lean.
import system.io
universes u v w
-----------------------------------------
View problem3.agda
module problem3 where
-- see:
-- https://www.reddit.com/r/DailyProver/comments/6d4oct/finite_cancellative_semigroups/
-- https://coq-math-problems.github.io/Problem3/
open import Relation.Binary.PropositionalEquality
open import Data.Product
Injective : {A B : Set} (f : A B) Set
View problem2.agda
module problem2 where
-- see https://np.reddit.com/r/DailyProver/comments/6brksy/infinite_valleys_and_the_limited_principle_of/
open import Data.Nat as Nat
import Data.Nat.Properties as NatProp
open import Data.Sum
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
View problem1.agda
module problem1 where
-- solution to https://coq-math-problems.github.io/Problem1/
--
-- sadly mine is the longest one
-- see https://www.reddit.com/r/Coq/comments/6amhkb/starting_a_problemoftheweek_blog_for_coq/
open import Data.Nat
import Data.Nat.Properties as NatProp
open import Data.Sum
View probability.hs
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
import Data.List
import Control.Monad
import Data.Function
import Numeric
formatFloatN floatNum numOfDecimals = showFFloat (Just numOfDecimals) floatNum ""
space = 10
You can’t perform that action at this time.