I hereby claim:
- I am omelkonian on github.
- I am omelkonian (https://keybase.io/omelkonian) on keybase.
- I have a public key whose fingerprint is F943 D15F CD25 12D0 0F70 90E0 5D31 C2DB 5A5B B4DB
To claim this, I am signing this object:
Orestis Melkonian omelkonian
🎰
omelkonian
/ Rose.agda
Last active
July 24, 2020 15:19
Different ways to recurse over rose trees and prove termination.
This file contains hidden or 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 Rose where | |
| open import Level | |
| open import Function | |
| open import Data.Empty | |
| open import Data.List | |
| open import Data.List.Membership.Propositional | |
| open import Data.List.Relation.Unary.Any using (Any; here; there) | |
| open import Data.Nat | |
| open import Data.Nat.Induction |
omelkonian
/ bracketings.hs
Created
October 27, 2018 21:50
This file contains hidden or 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 DeriveFoldable #-} | |
| data Tree a = Tree a :-: Tree a | V a deriving (Show, Eq, Foldable) | |
| allBr :: [a] -> [Tree a] | |
| allBr (x:x':xs) = ((V x :-: V x' :-:) <$> allBr xs) | |
| ++ ((V x :-:) <$> allBr (x':xs)) | |
| allBr xs = V <$> xs | |
| main :: IO () |