Instantly share code, notes, and snippets.

# Rotsor

Created July 9, 2019 22:36
A weird tree monad proposed on reddit
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 -- 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)
Last active May 15, 2018 20:04
Fulcrum in lean
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 -- 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 -----------------------------------------
Last active May 24, 2017 23:02
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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
Created May 21, 2017 17:32
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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
Created May 14, 2017 14:50
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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
Last active August 29, 2015 14:06 — forked from anonymous/probability.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE FlexibleInstances #-} import Data.List import Control.Monad import Data.Function import Numeric formatFloatN floatNum numOfDecimals = showFFloat (Just numOfDecimals) floatNum "" space = 10