KiJeong-Lim

module ndc.

kind parity type -> type -> type.
type pair (A -> B -> parity A B).

kind term type.
type fapp (string -> list term -> term).

kind formula type.
type atom (string -> list term -> formula).

KiJeong-Lim

import Control.Monad.IO.Class
import Control.Monad.Trans.Class
import Control.Monad.Trans.Except
import Control.Monad.Trans.State.Strict
import Data.IORef
import qualified Data.List as List
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import Data.Unique

KiJeong-Lim

Require Export Omega.
Require Export List.

Axiom classic : forall P : Prop, P \/ not P.

Module ListTheory.

  Section General.

    Import ListNotations.

KiJeong-Lim

{- https://gall.dcinside.com/mgallery/board/view/?id=github&no=14646 -}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Main where

import Data.Char
import System.Random
import Test.QuickCheck hiding ((.&.))

newtype BigChar
    = Big Char

KiJeong-Lim

module Main where

type Row = Int

type Col = Int

type Load = Double

type Deflection = Double

KiJeong-Lim

From Coq Require Export Bool.
From Coq Require Export PeanoNat.
From Coq Require Export Peano_dec.
From Coq Require Export List.

Module MyGroup.

  Section ClassDefns.

  Class Magma (G : Type) (plus : G -> G -> G) : Type :=

KiJeong-Lim

module Main where

import Control.Monad
import Data.Ratio
import Numeric.RootFinding

infix 7 <.>

at :: [a] -> Int -> a
list `at` index

KiJeong-Lim

From Coq.Bool Require Export Bool.
From Coq.micromega Require Export Lia.
From Coq.Lists Require Export List.
From Coq.Arith Require Export PeanoNat.

Module AuxiliaPalatina.  

  Import ListNotations.

  Section forNat.

KiJeong-Lim

From Coq.Bool Require Export Bool.
From Coq.micromega Require Export Lia.
From Coq.Lists Require Export List.
From Coq.Arith Require Export PeanoNat.
From Coq.Strings Require Export String.

Module Goedel's_Incompleteness_Theorem.

Import ListNotations.

KiJeong-Lim

#include <stdio.h>
#include <stdlib.h>
#define VM 30000

void solve13558(void)
{ typedef long long unsigned int llu_t;
  typedef short int val_t;
  int count_vi[VM], count_vk[VM];
  val_t ary[100000];
  llu_t res = 0;