kinoh

using System;
using System.Runtime.InteropServices;

namespace PortAudioSharp
{
    class PortAudioException : Exception
    {
        public PortAudioException(PaError err)
            : base(PortAudioAPI.Pa_GetErrorText(err))
        {

kinoh

using System;
using System.Collections.Generic;
using System.Linq;
using Irony.Parsing;

namespace IronySample
{
    public class MyGrammar : Grammar
    {
        public MyGrammar()

kinoh

1	1	0000->0001
2	2	0000->0001->0002
3	3	0000->0001->0002->0003
4	4	0000->0001->0002->0003->0004
5	5	0000->0001->0002->0003->0004->0005
6	6	0000->0001->0002->0003->0004->0005->0006
7	7	0000->0001->0002->0003->0004->0005->0006->0007
8	8	0000->0001->0002->0003->0004->0005->0006->0007->0008
9	9	0000->0001->0002->0003->0004->0005->0006->0007->0008->0009
10	10	0000->0001->0002->0003->0004->0005->0006->0007->0008->0009->0010

kinoh

$ A \in R $を左零因子とすると、ある$ B \in R \setminus \{0\} $が存在して$ AB = 0 $が成り立つ。
このとき$A$が可逆とすると$ A^{-1}AB = B = 0 $となり矛盾するから$ \det(A) = 0 $である。
$A$が右零因子の場合も同様にして$ \det(A) = 0 $である。
一方$ A \in R $について$ \det(A) = 0 $とすると、Gau\ss 消去により$ EA $の第$n$行が全て$0$となる様な基本行列$ E \in R $が存在する。
ここで更に$ B = \left( \begin{array}{c|c} O_{n-1} & 0 \\ \hline 0 & 1 \end{array} \right) $とおくと$ BEA = 0 $であり、基本行列は可逆なので$ \det(E) \ne 0 $より全て$0$の行は存在しない、よって特に$ n-1 $行には$0$でない要素が存在し$ BE \ne 0 $である。
故に$A$は右零因子である。
同様にGau\ss 消去を右基本変形で行えば$ \det(A) = 0 $のとき$A$が左零因子である事が分かる。
以上より$ A \in R $が左零因子である事と右零因子である事は同値である。

kinoh

A: {1..m} * {1..n} -> Field
for i in {1..m-1}
  k = max(k => abs(A[k,i]), {i..m})
  A = swap(A, i, k)
  for j in {i+1..m}
    A[j] -= (A[j,1] / A[i,1]) * A[i]

kinoh

use strict;

my $file = $ARGV[0];
my @data = ();

my @cast_types = ("AtomicOrdering", "SynchronizationScope", "BinOp", "BinaryOps", "Predicate", "OtherOps");
my @prim_types = ("bool", "unsigned", "unsigned short", "uint8_t", "uint16_t", "uint32_t", "uint64_t", "int8_t", "int16_t", "int32_t", "int64_t", "float", "double");

unlink "$file.h";
unlink "$file.cpp";

kinoh

using System;
using System.Collections.Generic;
using System.Linq;
using Irony.Parsing;
using LLVM;

namespace KaleidoScope
{
    [Language("KaleidoScope")]
    public class KaleidoScopeGrammar : Grammar

kinoh

<?xml version="1.0" encoding="utf-8" ?>
<Site Uri="http://www.kinokuniya.co.jp/f/dsg-01-" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema">
  <Preprocess xsi:type="Replace" Old="liitemprop" New="li itemprop"/>
  <Field Name="Title" Path="//h3[@itemprop='name']/text()[last()]" Pattern=".+"/>
  <Field Name="Label" Path="//h3[@itemprop='name']/text()[position()!=last()]" Pattern=".+"/>
  <Field Name="Authors" Path="//div[contains(@class,'infobox')]/ul/li[1]" Pattern="(?'name'[^/【】〈〉]+)(?=(?:〈(?'spell'[^〈〉]+)〉)?(?:/[^【]+)*【(?'role'[^】]+)】(?:〈(?'spell'[^〈〉]+)〉)?|$)"/>
  <Field Name="Publisher" Path="//div[contains(@class,'infobox')]/ul/li[count(./a)>0][last()]/a" Pattern=".+"/>
  <Field Name="Published" Path="//div[contains(@class,'infobox')]/ul/li[4]" Pattern="(?'year'\d{4})/(?'month'\d{2})発売"/>
  <Field Name="Size" Path="//div[contains(@class,'infbox')]/ul/li[1]" Pattern="サイズ (.+?)／"/>
  <Field Name="Page" Path="//div[contains(@class,'infbox')]/ul/li[1]" Pattern=

kinoh

(* https://www.fstar-lang.org/tutorial/ *)
module FoldLeft

val append : list 'a -> list 'a -> Tot (list 'a)
let rec append l1 l2 = match l1 with
  | [] -> l2
  | hd :: tl -> hd :: append tl l2

val reverse: list 'a -> Tot (list 'a)
let rec reverse = function 

kinoh

module Range

val length: list 'a -> Tot nat
let rec length l =
	match l with
	| [] -> 0
	| _::tl -> 1 + length tl

val range: a:nat -> b:nat -> Tot (list nat)
			(decreases (b-a))