gergoerdi

{-# LANGUAGE GADTs, TypeInType, DataKinds, TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}

import GHC.TypeLits
import GHC.Types
import Data.Singletons
import Data.Singletons.Prelude

data Format = Lit Symbol | Str | Shown Type

gergoerdi

import Distribution.Simple
import Distribution.Simple.BuildTarget
import Distribution.Simple.LocalBuildInfo
import Distribution.Simple.Setup
import Distribution.Types.ComponentRequestedSpec

import Distribution.Types.Lens
import Data.List (sort, nub)
import Control.Monad (when, forM_)
import System.Directory

gergoerdi

liftTypeRep :: TypeRep a -> TH.Type
liftTypeRep ty = L.foldl AppT t0 [liftTypeRep ty' | SomeTypeRep ty' <- args]
  where
    (con, args) = splitApps ty
    t0 = ConT $ mkName (tyConModule con <> "." <> tyConName con)

gergoerdi

traverseTerm : (Applicative f) => (Var vars1 -> f (Term vars2)) -> (Term vars1 -> f (Term vars2))
traverseTerm go (Local idx p) = go (MkVar p)
traverseTerm go (Ref nt x) = pure $ Ref nt x
traverseTerm go (Meta x ts) = Meta x <$> traverse (traverseTerm go) ts
traverseTerm go (Bind x b scope) = Bind x <$> traverse (traverseTerm go) b <*> traverseTerm go' scope
  where
    go' : Var (x :: vars1) -> f (Term (x :: vars2))
    go' (MkVar First) = pure $ Local _ First
    go' (MkVar (Later p)) = weaken <$> go (MkVar p)
traverseTerm go (App f e) = App <$> traverseTerm go f <*> traverseTerm go e

gergoerdi

function r(e) {

 

    var n =

        [[1.11e11, 0.6819],

         [8.12e10, 0.6518],

gergoerdi

-- https://stackoverflow.com/a/57046042/477476
-- https://gist.github.com/Lysxia/7331df3abee0aceacd3d9a74b567f54c

{-# LANGUAGE RankNTypes, TypeFamilies, PolyKinds, DataKinds #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs, TypeOperators #-}
{-# LANGUAGE TypeApplications, RebindableSyntax #-}

import Prelude hiding (id, (.))
import Control.Category

gergoerdi

-- https://stackoverflow.com/a/57046042/477476
-- https://gist.github.com/Lysxia/04039e4ca6f7a3740281e4e3583ae971

{-# LANGUAGE RankNTypes, TypeFamilies, PolyKinds, DataKinds #-}
{-# LANGUAGE GADTs, TypeOperators #-}
{-# LANGUAGE TypeApplications, RebindableSyntax, RecordWildCards #-}

import Prelude hiding (id, (.))
import Control.Category
import Data.Kind

gergoerdi

-- https://stackoverflow.com/a/57046042/477476
-- https://gist.github.com/Lysxia/04039e4ca6f7a3740281e4e3583ae971

{-# LANGUAGE RankNTypes, TypeFamilies, PolyKinds, DataKinds #-}
{-# LANGUAGE TypeApplications, TypeOperators, GADTs #-}

import Prelude hiding (id, (.))
import Control.Category
import Data.Kind
import GHC.TypeLits

gergoerdi

{-# OPTIONS --cubical #-}
module Int where

open import Data.Nat renaming (_+_ to _+̂_)
open import Cubical.Core.Prelude
open import Utils

Same : ℕ → ℕ → ℕ → ℕ → Set
Same x y x′ y′ = x +̂ y′ ≡ x′ +̂ y

gergoerdi

{-# OPTIONS --cubical #-}
module Quotient where

open import Cubical.Core.Prelude

Reflexive : ∀ {ℓ} {A : Set ℓ} → (A → A → Set ℓ) → Set _
Reflexive _∼_ = ∀ x → x ∼ x

module Quot {ℓ} (A : Set ℓ) (_∼_ : A → A → Set ℓ) (∼-refl : Reflexive _∼_) where
  data Q : Set ℓ where