yfyf

.module example

.custom-field erlang-type-prefix
.erlang-type-prefix ""

.alias [
    .name itemid
    .type uint32
]
.record [

yfyf

### output of ./configure && make deps && make

checking whether necessary dependencies are already installed...
xmlm is installed in /usr/lib/ocaml/xmlm
ulex is installed in /usr/lib/ocaml/ulex
easy-format is installed in /usr/lib/ocaml/easy-format
mkdir -p /home/yfyf/sandbox/piqi/build/lib/ocaml
make -C deps
make[1]: Entering directory '/home/yfyf/sandbox/piqi/deps'
set -e; \

yfyf

-- Tooltip comes from: https://github.com/liliff/web/blob/master/_posts/2012-04-05-first-dive-into-lua-battery-widget.md

function rgbToHex(r, g, b)
    return string.format("#%0.2X%0.2X%0.2X", r, g, b)
end

function chargeToColour(charge)
    local unit = 255 / 100
    local amount = math.floor(unit * charge)
    return rgbToHex(255 - amount, amount, 25)

yfyf

/*
 * Byte calculator. Sums bytes of a given file and displays to screen.
 *
 * Compile:
 *  gcc ccalc.c -o ccalc -O2
 *
 */
#include <stdlib.h>
#include <stdio.h>
#include <stdint.h>

yfyf

# there's probably a nicer way to do this, but anyway:

# path where to hold the last cwd
SUPER_CWD_FILE=/tmp/scwd

# store the cwd on each command
export PROMPT_COMMAND="pwd > $SUPER_CWD_FILE; $PROMPT_COMMAND"

# restore the cwd when starting a new shell
[ -r $SUPER_CWD_FILE ] && cd `cat $SUPER_CWD_FILE`

yfyf

Skipping ./ConcEnv.idr
Type checking ./ConcState.idr
ConcState.idr:134:Can't unify EffM IO effs effs () with EffM IO [(MkEff
    (ConcEnv ResState Resource rsin) eff)] xs' ()

Specifically:
    Can't unify effs with [MkEff (ConcEnv ResState Resource rsin) eff]
    ConcState.idr:176:Incomplete term Effects.>>= {m = IO} {xs = [MkEff
    (ConcEnv {n = 1} ResState Resource [(RState Z Nat)]) (ConcState
    IO),MkEff () StdIO]} {xs' = updateWith {a = EFFECT} {ys = [MkEff

yfyf

module Issue

data Env : (t: Type) -> (iR: t -> Type) -> (xs: Vect t n) -> Type where
   Empty : {iR: t -> Type} -> (Env t iR Vect.Nil)
   Extend : {r:t} -> {iR: t -> Type} -> {xs: Vect t n} ->
                (res: (iR r)) -> (Env t iR xs) -> (Env t iR (r::xs))

data ElemAtIs : (i: Fin n) -> a -> Vect a n -> Type where
  ElemAtIsHere : {x: a} -> {xs : Vect a n} -> ElemAtIs fO x (x::xs)
  ElemAtIsThere : {i : Fin n} -> {x: a} -> {xs : Vect a n} ->

yfyf

-module(refl).

-compile(export_all).

normal(Foo) ->
    lists:sort([Foo]).

bad(Mod, Fun, Foo) ->
    Mod:Fun([Foo]).

yfyf

-define(FULL_EUNIT_OUTPUT(Expr),
   begin
       try Expr
       catch
           _:Foo ->
               ?debugFmt("~n~100P~n", [Foo, 999999]),
               erlang:error(eunit_assert_failed)
       end
   end).

yfyf

%% If your shell is setup correctly then inputing unicode chars should work like this:
1> A = "žžžūvis".
[382,382,382,363,118,105,115]
%% Contains integers > 255,
%% hence this is a list of codepoints, good!

%% None of these will work:
17> <<"žžžūvis">>.
** exception error: bad argument
18> <<"žžžūvis"/utf8>>.