{{ message }}

Instantly share code, notes, and snippets.

# István Donkó Isti115

Last active Sep 20, 2021
Normalization proof for SK combinator calculus using Agda
View sknorm.agda
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
 {-# OPTIONS --rewriting #-} module sknorm where open import Agda.Primitive open import Level open import Relation.Binary.PropositionalEquality open import Agda.Builtin.Equality.Rewrite open import Data.Product open import Data.Empty
Created Apr 24, 2021
Fix the Discord authentication issue with differing inner and outer widths (e.g. QuteBrowser tabs on the left)
View discord-auth-fix.user.js
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
 // ==UserScript== // @name Discord Auth Fix // @namespace http://istvan.donko.hu/ // @version 0.1 // @description Fix Discord auth issue with window sizing // @author István Donkó (Isti115) // @match https://discord.com/* // @run-at document-start // ==/UserScript==
Created Mar 29, 2021
Haskell solution for Median Sort interactive problem from the Qualification Round of Google Code Jam 2021
View MedianSort.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 DeriveFoldable #-} import System.IO import Control.Monad import Data.Foldable data Tree a = Leaf | Node (Tree a) a (Tree a) deriving (Foldable) singleton :: a -> Tree a singleton a = Node Leaf a Leaf
Created Sep 13, 2020
View agda.sh
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
 AGDA_STDLIB=/usr/share/agda-stdlib # build() # # Available: # - submission: the text of submission (file) # - tests: test cases (file) # - SANDBOX_PATH: root of the directory where run() will be invoked build() { name=\$(cat tests | grep -m 1 -oP "(?<=module ).*(?= where)")
Created Jun 19, 2020
Proof of concept blender addon for controlling the viewport with a gamepad (evdev python module needed, only tested under linux)
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
 bl_info = { "name" : "Gamepad Control", "author" : "István Donkó", "description" : "Control the blender viewport using a gamepad", "blender" : (2, 80, 1), # "location" : "View3D", "category" : "Generic" } import bpy
Last active May 18, 2020
Pulseaudio mirophone output feedback problem
View amixer-c1.txt
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
 Simple mixer control 'Master',0 Capabilities: pvolume pvolume-joined pswitch pswitch-joined Playback channels: Mono Limits: Playback 0 - 87 Mono: Playback 61 [70%] [-19.50dB] [on] Simple mixer control 'Headphone',0 Capabilities: pvolume pswitch Playback channels: Front Left - Front Right Limits: Playback 0 - 87 Mono:
Last active Apr 30, 2020
Hilbert system formalization in Agda
View Hilbert.agda
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 Hilbert where -- postulate -- Identifier : Set -- a b c x y z : Identifier -- bot : Identifier infixr 4 _=>_ data Expression : Set where
Created Dec 30, 2019
View cursor.ahk
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
 #SingleInstance force ;#NoTrayIcon Menu, Tray, Icon, C:\Users\isti\programming\AutoHotKey\icons\cursor.ico ;#If GetKeyState("CapsLock", "P") ; --- Space #If GetKeyState("vkE2", "P") && GetKeyState("Space", "P")
Created Sep 5, 2018
AutoHotKey script mainly for cursor navigation without leaving the area around the home row. It uses the extra key next to "z" on a 102 key keyboard.
View Cursor.ahk
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
 #SingleInstance force ;#NoTrayIcon Menu, Tray, Icon, C:\Users\isti\programming\AutoHotKey\icons\cursor.ico ;#If GetKeyState("CapsLock", "P") ; --- Space #If GetKeyState("vkE2", "P") && GetKeyState("Space", "P")