KiJeong-Lim

module BlockArgument where
import qualified Control.Monad.Trans.Class as Y
import qualified Control.Monad.Trans.Except as Y
import qualified Control.Monad.Trans.State.Strict as Y
import qualified Data.Map.Strict as YMap
import qualified Data.Set as YSet

data Tok
    = LargeId String
    | SmallId String

KiJeong-Lim

module Sudoku where

import Control.Monad
import Data.List

type Grid = [[Int]]

solveSudoku :: Grid -> [Grid]
solveSudoku = foldr (<=<) return go where
    go :: [Grid -> [Grid]]

KiJeong-Lim

Section MU_RECURSIVE.

#[local] Close Scope list_scope.
#[local] Open Scope vector_scope.

Let arity : Set := nat.

Inductive MuRec : arity -> Set :=
  | MR_succ : MuRec 1
  | MR_zero : MuRec 0

KiJeong-Lim

module Main where

type Lit = Int

data Expr
    = And Expr Expr
    | Xor Expr Expr
    | Add Expr Expr
    | Zero
    | Unit

KiJeong-Lim

couldn't resolve conflict:
  ? REDUCE: <TypeConstructorName> ::= `largeid'; v.s. REDUCE: <TypeClassName> ::= `largeid'; at { state = 14, terminal = `smallid' }
  ? collection = {
    getParserSInfo :: ParserS -> ParserSInfo
    getParserSInfo 0 = ParserSInfo
        { myItems = 
            [ "<PiType> ::= . <TauType>"
            , "<PiType> ::= . `lparen' <Sequence Contraint> `rparen' `fatarrow' <TauType>"
            , "<TauType> ::= . <TauType1>"
            , "<TauType> ::= . <TauType1> `arrow' <TauType>"

KiJeong-Lim

#include <cstdint>
#include "scratch.hpp"

struct MotorInput {
    float p;
    float v;
    float kp;
    float kd;
    float t_ff;
};

KiJeong-Lim

(* "A category-theoretical approach to the definition of bisimulation map between labelled-transition systems"
  [#1]
  ```coq
  Section TMP_SECT_1.
  Definition ensemble (A : Type) : Type := A -> Prop.
  Definition member {A : Type} : A -> ensemble A -> Prop := fun x : A => fun X : ensemble A => X x.
  Variable Eff : Type.
  Inductive my_map {A : Type} {B : Type} (f : A -> B) (X : ensemble (A * Eff)) : ensemble (B * Eff) :=
  | in_my_map : forall a : A, forall e : Eff, member (a, e) X -> member (f a, e) (my_map f X)
  .

KiJeong-Lim

[The chain of command]

                                                  +------- Motor #1
                                                  |
                +--------- Transceiver #1 --------+------- Motor #2
                |                                 |
                |                                 +------- Motor #3
                |
Nucleo ---------+
                |

KiJeong-Lim

(* 자연연역의 monotonicity 성질을 coq으로 형식증명하다가 질문이 생겼습니다. *)

(* 먼저 저는 자연연역을 다음과 같이 정의했습니다. *)
Inductive infers {L: language} (Gamma: ensemble (@frm L)) : forall C: (@frm L), Prop :=
| By_hyp p
  (IN: p \in Gamma) (* p가 Gamma의 원소일 때 *)
  : Gamma ⊢ p       (* Gamma ⊢ p이다 *)
| (* ... *)
| Forall_intro x y p1
  (NOT_FREE1: is_not_free_in_frms y Gamma)                   (* y가 Gamma에 자유롭게 나타나는 개체변수가 아니고)

KiJeong-Lim

module Main where

import Control.Monad.Trans.Class
import Control.Monad.Trans.Cont

foo :: ContT r IO String
foo = callCC $ \k -> do
    b <- lift $ readLn
    if b then k "early return" else return ()
    lift $ putStrLn "Hello world!"