Paulo Torrens takanuva
david-christiansen
/ PlusRewrite.idr
Last active
August 8, 2016 20:31
Simplifying "plus" expressions with rewrite-rule combinators and quasiquotes in Idris
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 PlusRewrite | |
| import Language.Reflection | |
| import Language.Reflection.Utils | |
| rewrite_plusSuccRightSucc : TT -> Maybe Tactic | |
| rewrite_plusSuccRightSucc `(plus ~n (S ~m)) = Just $ Rewrite `(plusSuccRightSucc ~n ~m) | |
| rewrite_plusSuccRightSucc `(S ~n) = rewrite_plusSuccRightSucc n | |
| rewrite_plusSuccRightSucc `(plus ~n ~m) = rewrite_plusSuccRightSucc n <|> rewrite_plusSuccRightSucc m | |
| rewrite_plusSuccRightSucc _ = Nothing |
greenboxal
/ gist:6346759
Created
August 26, 2013 21:16
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
| Address Ordinal Name Library | |
| ------- ------- ---- ------- | |
| 4A781000 AllocateAndInitializeSid ADVAPI32 | |
| 4A781004 InitializeAcl ADVAPI32 | |
| 4A781008 RegCloseKey ADVAPI32 | |
| 4A78100C RegOpenKeyExW ADVAPI32 | |
| 4A781010 GetTokenInformation ADVAPI32 | |
| 4A781014 GetLengthSid ADVAPI32 | |
| 4A781018 LsaLookupNames ADVAPI32 | |
| 4A78101C AddAccessAllowedAce ADVAPI32 |
twanvl
/ Sorting.agda
Last active
December 2, 2022 16:44
Correctness and runtime of mergesort, insertion sort and selection sort.
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 Sorting where | |
| -- See https://www.twanvl.nl/blog/agda/sorting | |
| open import Level using () renaming (zero to ℓ₀;_⊔_ to lmax) | |
| open import Data.List hiding (merge) | |
| open import Data.List.Properties | |
| open import Data.Nat hiding (_≟_;_≤?_) | |
| open import Data.Nat.Properties hiding (_≟_;_≤?_;≤-refl;≤-trans) | |
| open import Data.Nat.Logarithm | |
| open import Data.Nat.Induction |
folone
/ HindleyMilner.scala
Last active
December 17, 2015 01:49
I thought, this: http://dysphoria.net/code/hindley-milner/HindleyMilner.scala needs a home.
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
| /* | |
| * http://dysphoria.net/code/hindley-milner/HindleyMilner.scala | |
| * Andrew Forrest | |
| * | |
| * Implementation of basic polymorphic type-checking for a simple language. | |
| * Based heavily on Nikita Borisov’s Perl implementation at | |
| * http://web.archive.org/web/20050420002559/www.cs.berkeley.edu/~nikitab/courses/cs263/hm.html | |
| * which in turn is based on the paper by Luca Cardelli at | |
| * http://lucacardelli.name/Papers/BasicTypechecking.pdf | |
| * |
t0yv0
/ subtyping.v
Last active
August 27, 2025 17:43
Demonstrating TypeScript 0.8 type system to be unsound. The subtyping relationship is defined in a way that admits the following code that results in TypeError exception being thrown.
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
| Require Import Utf8. | |
| Inductive subtype (a b : Set) : Set := | |
| | ST : (a -> b) -> subtype a b. | |
| Infix ":>" := subtype (at level 50). | |
| Definition st {x y} f := ST x y f. | |
| Definition unpack {a b : Set} (st : a :> b) := |
NewerOlder