konn

@require: easytable/easytable
@require: stdja
@require: ncsq/ncsq

document (|
  title = {ほげふが};
  author = {};
  show-title = true;
  show-toc = true;
|) '<

konn

let const a _ = a
let always-zero = const 0
let _ = always-zero (always-zero true) % Error!
%                   ^~~~~~~~~~~~~~~~~
%                     Type Error
%                     this expression has type
%                       int,
%                     but is expected of type
%                       bool.

konn

@require: stdjareport
@require: math
document (|
  title = {あああああ};
  author = {mr_konn};
  date = {2022/04/23};
|) '<
+chapter{あああああ}<
  +proof{
    ううううううう

konn

Require Import Arith.

Theorem plus_assoc_r: forall l n m : nat, l + (m + n) = (l + m) + n.
Proof.
  intros.
  induction l.
  rewrite plus_0_l.
  rewrite plus_0_l with (n := m).
  reflexivity.
  rewrite plus_Sn_m.

konn

module FOL
import Syntax.PreorderReasoning

succAndOne : (n : Nat) -> plus n 1 = S n
succAndOne n = ?succAndOne_rhs

record Language : Type where
  LanguageDef : (funSym : Type)-> (predSym : Type) ->
                (funArity : funSym -> Nat) -> (predArity : predSym -> Nat) -> Language

konn

{-# LANGUAGE DataKinds, ExistentialQuantification, FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances, GADTs, IncoherentInstances, InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses, PolyKinds, RankNTypes                #-}
{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TemplateHaskell    #-}
{-# LANGUAGE TypeApplications, TypeFamilies, TypeInType, TypeOperators   #-}
{-# LANGUAGE UndecidableInstances, UnicodeSyntax                         #-}
module Main where
import GHC.TypeLits
import Data.Kind
import Data.Singletons.Prelude

konn

$ stack ghci --verbose
Version 2.5.1, Git revision d6ab861544918185236cf826cb2028abb266d6d5 x86_64 hpack-0.33.0
2021-01-29 22:44:07.844116: [debug] Checking for project config at: /Users/hiromi/Documents/Programming/Haskell/git/hls-conditional-modules/stack.yaml
2021-01-29 22:44:07.844573: [debug] Loading project config file stack.yaml
2021-01-29 22:44:07.849169: [debug] (SQL) SELECT COUNT(*) FROM "last_performed" WHERE ("action"=?) AND ("timestamp">=?); [PersistInt64 1,PersistUTCTime 2021-01-28 13:44:07.849126 UTC]
2021-01-29 22:44:07.850659: [debug] Using package location completions from a lock file
2021-01-29 22:44:07.852246: [debug] Loaded snapshot from Pantry database.
2021-01-29 22:44:08.007014: [debug] RawSnapshotLayer {rslParent = RSLCompiler (WCGhc (mkVersion [8,10,3])), rslCompiler = Nothing, rslLocations = [RPLIHackage AC-Angle-1.0@sha256:e1ffee97819283b714598b947de323254e368f6ae7d4db1d3618fa933f80f065,544 (Just (TreeKey 7edd1f1a6228af27c0f0ae53e73468c1d7ac26166f2cb386962db7ff021a2714,210)),RPLIHa

konn

{-# LANGUAGE ConstraintKinds, DataKinds, DeriveGeneric, DerivingVia    #-}
{-# LANGUAGE ExplicitNamespaces, FlexibleContexts, FlexibleInstances   #-}
{-# LANGUAGE GADTs, GeneralizedNewtypeDeriving, MultiParamTypeClasses  #-}
{-# LANGUAGE PolyKinds, ScopedTypeVariables, StandaloneDeriving        #-}
{-# LANGUAGE TypeApplications, TypeFamilies, TypeInType, TypeOperators #-}
{-# LANGUAGE UndecidableInstances                                      #-}
{-# OPTIONS_GHC -Wall #-}
module Data.Aeson.Generic.DerivingVia
     ( StrFun(..), Setting(..), SumEncoding'(..), DefaultOptions, WithOptions(..)
     , -- Utility type synonyms to save ticks (') before promoted data constructors

konn

{-# LANGUAGE DuplicateRecordFields, OverloadedStrings, RecordWildCards #-}
module JSaddleCompat (runApp, App(..)) where
import qualified Language.Javascript.JSaddle.Warp as JSaddle
import           Miso                             (startApp, syncPoint)
import qualified Miso                             as Miso
import           Network.HTTP.Client.Conduit      (Manager, newManager)
import           Network.HTTP.ReverseProxy        (WaiProxyResponse (..),
                                                   defaultOnExc, waiProxyTo)
import           Network.Wai                      (Application, pathInfo)
import qualified Network.Wai.Handler.Warp         as Warp

konn

{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, PolyKinds     #-}
{-# LANGUAGE RankNTypes, RecordWildCards, StandaloneDeriving, TypeFamilies #-}
{-# LANGUAGE UndecidableInstances                                          #-}
module Lib where
import Data.Functor.Identity
import Options.Applicative

someFunc :: IO ()
someFunc = putStrLn "someFunc"