littlebenlittle

module _ where

data _≡_ {A : Set} : A → A → Set where
  refl : ∀ (x : A) → x ≡ x

data GroupAxioms {A : Set} (id : A) (inv : A → A) (op : A → A → A) : Set where
  GroupAxioms! :
      ∀ (x : A) → op x id ≡ x
    → ∀ (x : A) → op id x ≡ x
    → ∀ (x : A) → op x (inv x) ≡ id

littlebenlittle

#|(
 Match against an infinite family of <!before> patterns
)

say 'x_x___x________' ~~ /
[
| 'x'
| '_' <!before [
        | $ 
        | '_' <?before $> 

littlebenlittle

module _ where

-- Constructive Set
data CSet {A : Set} : (A → Set) → Set where
  ⟨_⟩  : (p : A → Set) → CSet p

data _∈_ {A : Set} {p : A → Set} (x : A) (S : CSet p) : Set where
  ∈-pf : p x → x ∈ S

littlebenlittle

### Keybase proof

I hereby claim:

  * I am littlebenlittle on github.
  * I am benlittle (https://keybase.io/benlittle) on keybase.
  * I have a public key ASCMAixeMyR_wrla6Qsd_zlEme2cSl2AS-tm94lew4APlAo

To claim this, I am signing this object:

littlebenlittle

#| Generate a 5 word phrase. NOT crypto random.
'/usr/share/dict/cracklib-small'.IO.lines».lc.pick(5).join(' ').say;

littlebenlittle

zero.
nat(zero).
nat(X) :-
	nat(Y),
	suc(Y,X).

one.
suc(zero,one).

littlebenlittle

===RUNNING zef --debug install
install OUT:

install ERR:
Usage:
  zef [--fetch] [--build] [--test] [--depends] [--test-depends] [--build-depends] [--force] [--force-resolve] [--force-fetch] [--force-extract] [--force-build] [--force-test] [--force-install] [--timeout=<Int>] [--fetch-timeout=<Int>] [--extract-timeout=<Int>] [--build-timeout=<Int>] [--test-timeout=<Int>] [--install-timeout=<Int>] [--degree=<Int>] [--fetch-degree=<Int>] [--test-degree=<Int>] [--dry] [--upgrade] [--deps-only] [--serial] [--contained] [--update=<Any>] [--exclude=<Any>] [--to|--install-to=<Any>] install [<wants> ...] -- Install

===RUNNING zef --debug uninstall
uninstall OUT:

littlebenlittle

use v6;

my @sub-commands = «
    install
    uninstall
    test
    fetch
    build
    look
    update

littlebenlittle

use v6;

grammar Test {
    token TOP { <x>+ % \h+ $<rest>=(.*) }
    proto token x {*}
    token x:sym<A> { \S+ [\h \S+]* }
    token x:sym<B> {
        "[" <special-token> "]" <.ws> <important-message>
    }
    token special-token { "SPECIAL TOKEN" }

littlebenlittle

# based on https://stackoverflow.com/a/60512071/5530704

module Tabular {

    grammar Data {
        token TOP {
            <header-row>    \n
            <value-row>+ %% \n
        }
        token header-row { <.ws>+ %% <symbol> }