RyanGlScott

allow-newer:
  aeson:containers,
  aeson:template-haskell,
  -- Ugh.
  aeson:th-abstraction,
  assoc:base,
  async:base,
  -- TODO
  bifunctors:template-haskell,
  binary-orphans:base,

RyanGlScott

constraints:
  containers == 0.7.*

allow-newer:
  aeson:containers,
  Cabal-syntax:containers,
  cabal-install-parsers:containers,
  cassava:containers,
  foldable1-classes-compat:containers,
  hashable:containers,

RyanGlScott

crux-mir
  crux concrete
    
      refs
        promoted_imm:            OK (0.15s)
          Compiling and running oracle program (0.15s)
          Oracle output: 0
          Crux output: 0
        mut_raw:                 OK (0.15s)
          Compiling and running oracle program (0.15s)

RyanGlScott

module Blah where

RyanGlScott

allow-newer:
  aeson:deepseq,
  aeson:ghc-prim,
  aeson:template-haskell,
  aeson:th-abstraction,
  assoc:base,
  async:base,
  attoparsec:ghc-prim,
  binary-orphans:base,
  boring:base,

RyanGlScott

From Coq Require Import Program.Basics.
From Coq Require        Program.Equality.
From Coq Require Import Vectors.Vector.
From Coq Require Import Logic.Eqdep.

Import VectorNotations.

Require Import Lia.
Require Import ZArith.
Require Import ZifyBool.

RyanGlScott

From Coq Require Import Program.Basics.
From Coq Require        Program.Equality.
From Coq Require Import Vectors.Vector.
From Coq Require Import Logic.Eqdep.

Import VectorNotations.

Require Import Lia.
Require Import ZArith.
Require Import ZifyBool.

RyanGlScott

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module HDList where

import qualified Control.Category as Cat (Category(..))
import Data.Function (on)

RyanGlScott

Require Import Lists.List.
Import ListNotations.
Open Scope list_scope.
Require Import Logic.FunctionalExtensionality.
Require Import Lists.Streams.

Inductive DList (a : Type) : Type :=
| MkDList : (list a -> list a) -> DList a.
Arguments MkDList {a} f.

RyanGlScott

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module FromToVec where