damhiya

From Coq Require Fin.

Definition ifun (X Y : nat -> Type) : Type := forall i, X i -> Y i.
Definition δ (X : nat -> Type) (n : nat) := X (S n).
Definition prod (X Y : nat -> Type) (n : nat) := (X n * Y n)%type.
Definition sum (X Y : nat -> Type) (n : nat) := (X n + Y n)%type.

Definition TermF' (X : nat -> Type) := sum (δ X) (prod X X).

Variant TermF (X : nat -> Type) : nat -> Type :=

damhiya

CoInductive bits : Set :=
| c0 : bits -> bits
| c1 : bits -> bits.

Lemma bits_eta : forall xs, match xs with
                     | c0 xs' => c0 xs'
                     | c1 xs' => c1 xs'
                     end = xs.
Proof.
  intro xs. destruct xs; reflexivity.

damhiya

data I = T | F
data TreeF :: (I -> Type) -> (I -> Type) where
  Tip    :: Int -> TreeF f T
  Forest :: f F -> TreeF f T
  Nil    :: TreeF f F
  Cons   :: f T -> f F -> TreeF f F

data Tree :: I -> Type where
  Fold :: TreeF Tree i -> Tree i

damhiya

let and = fn (b1 : bool) -> fn (b2 : bool) ->
            if b1 then b2 else false in
let or =  fn (b1 : bool) -> fn (b2 : bool) ->
            if b1 then true else b2 in
let map = fn (f : int * int * int -> int * int * int) ->
          fix (mapf : list (int * int * int) -> list (int * int * int)) xs ->
            case xs of
              { [] -> [] of (int * int * int)
              ; x :: xs -> f x :: mapf xs
              } in

damhiya

# Tetrahedron
# volume = 1/6
# area = (3 + sqrt 3)/2

tetrahedronMesh =
    let vmap = [ 0. 1. 0. 0.
               ; 0. 0. 1. 0.
               ; 0. 0. 0. 1.
               ]
        fmap = [ 0 0 0 1

damhiya

회전

회전에 대해 알아보자. 2차원에선 간단하지. 점 $(x,y)$를 $\theta$만큼 회전시킨 좌표 $(x',y')$은 이렇게 표현이 돼.

$$ \begin{pmatrix} x' \ y' \end{pmatrix} = \begin{pmatrix} \cos \theta & \sin \theta \

damhiya

#!/usr/bin/env bash
PROFILE_PATH=/nix/var/nix/profiles

get_list() {
  find $PROFILE_PATH -type l \
  | awk "match(\$0, /^${PROFILE_PATH//\//\\\/}\/system-([0-9]*)-link\$/, res) { print res[1] }" \
  | sort
}

get_current() {

damhiya

{
  inputs = {
    nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable";
    flake-utils.url = "github:numtide/flake-utils";
  };

  outputs = { self, nixpkgs, flake-utils }:
    flake-utils.lib.eachDefaultSystem (system:
      let
        pkgs = import nixpkgs { inherit system; };

damhiya

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs          #-}

module Main where

import GHC.Types
import Control.Monad

type Coffee = Integer
type Work = Integer

damhiya

{-# LANGUAGE ExplicitForAll      #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Rose where

data Tree a = Node a [Tree a] deriving (Eq, Show)

t1 :: Tree Int
t1 = Node 1
       [ Node 2