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

gergoerdi

open import Agda.Builtin.FromNat
open import Data.Fin

open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Data.Nat renaming (_≤?_ to _N≤?_)
open import Data.Unit

instance
  NumFin : ∀ {n} → Number (Fin n)

gergoerdi

open import Data.Nat
open import Relation.Binary.PropositionalEquality renaming (subst to ≡-subst)
open import Data.Empty
open import Data.Unit
open import Relation.Binary
open import Data.Star
open import Level renaming (zero to lzero; suc to lsuc)
open import Data.Product
open import Function using (_⟨_⟩_)
-- open import Function using (_∘_; id)

gergoerdi

#include "sim_avr.h"
#include "avr_ioport.h"
#include "sim_elf.h"

#include <stdio.h>

void ext_cb(struct avr_irq_t* irq, uint32_t val, void* closure)
{
    avr_irq_t *trigger = (avr_irq_t*)(closure);