t0yv0

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) :=

folone

/*
 *  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
 *

twanvl

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

greenboxal

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

david-christiansen

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

agrif

-- Exercise: prove Peirce’s law <=> law of excluded middle in Haskell
 
{-# LANGUAGE Rank2Types #-}
 
import Data.Void
import Data.Bifunctor
import Data.Functor.Identity
 
type Not a = a -> Void

fay59

Here's a list of mildly interesting things about the C language that I learned mostly by consuming Clang's ASTs. Although surprises are getting sparser, I might continue to update this document over time.

There are many more mildly interesting features of C++, but the language is literally known for being weird, whereas C is usually considered smaller and simpler, so this is (almost) only about C.

1. Combined type and variable/field declaration, inside a struct scope [https://godbolt.org/g/Rh94Go]

struct foo {
   struct bar {
 int x;

rxwei

See the official Differentiable Programming Manifesto instead.

racerxdl

jtag newtap ecp5 tap -irlen 8 -expected-id 0x41111043

Gadgetoid

CFLAGS_ALL=-I../libusbgx/build/include -I../bcm2835-1.68/build/include -L../bcm2835-1.68/build/lib -I../lua-5.4.0/src -L../libusbgx/build/lib -L../libserialport/build/lib -L../lua-5.4.0/src -lpng -lz -lpthread -llua -lm -lbcm2835 -ldl

pi400: CFLAGS+=-static $(CFLAGS_ALL) -lusbgx -lconfig -DPI400_USB
pi400: pi400.c gadget-hid.c
	$(CC)  $^ $(CFLAGS) -o $@


pi400test: CFLAGS+=-static $(CFLAGS_ALL) -lusbgx -lconfig
pi400test: pi400.c gadget-hid.c
	$(CC)  $^ $(CFLAGS) -o $@