elefthei

From Ltac2 Require Import Ltac2.

Section Ltl.
  Context {X W: Type} (step: X -> W -> X -> W -> Prop).
  Notation XP := (X -> W -> Prop).

  Definition lnext(φ: XP): XP :=
    fun x w => exists x' w', step x w x' w' /\ φ x' w'.
  Arguments lnext: simpl never.
  Opaque lnext.

elefthei

From Coq Require Import Unicode.Utf8.
From Coq Require Import Arith.

Section CoquandCompContext.
  Hypothesis f: nat -> nat.
  Context (x0: nat).
  Hypothesis H1: forall x, exists y, x < f y.
  Hypothesis H2: f 0 <= x0.

  Definition P := exists n, f n <= x0 /\ x0 < f (S n).

elefthei

import numpy as np

elefthei

From Coq Require Import Vectors.VectorDef.
From Coq Require Import micromega.Lia.
From Coq Require Import Program.Basics Program.Equality.
From Coq Require Import Arith.PeanoNat.

Import VectorNotations.
Open Scope program_scope.

Definition vec := t.

elefthei

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
import           Control.Monad.State.Lazy

-- Inner Monad (Bar)
data BarState = BarState { bars :: [Char] }
newtype Bar a = Bar (State BarState a) deriving (Functor, Applicative, Monad, MonadState BarState)

elefthei

package Interpreters

import scala.collection.immutable.HashMap

object LMapOps {

  // Let's construct expressions for a lazy HashMap
  sealed trait LMap[F, U] extends Product with Serializable {
    // Implement these
    def run: HashMap[F, U]

elefthei

(** Arrays in coq*)
Set Implicit Arguments.

Module Array.

(** arrays as a monad. Coq typechecker does not allow `get` to be `array T -> nat -> T` as it should
 and requires the wrong type `array T -> nat -> array T` to always terminate in `array T`. *)
  Inductive array: Type -> Type :=
    | get: forall T, array T -> nat -> array T
    | put: forall T, array T -> nat -> T -> array T

elefthei

Set Implicit Arguments.

Inductive proc: Type -> Type :=
| ret: forall T, T -> proc T
| bind: forall T T', proc T -> (T -> proc T') -> proc T'
| print: nat -> proc unit.



Fixpoint f(a: nat) :=

elefthei

#define XTL_DEFAULT_SYNTAX 'S'

#include <iostream>
#include <mach7/type_switchN-patterns.hpp> // Support for N-ary Match statement on patterns
#include <mach7/patterns/address.hpp>      // Address and dereference combinators
#include <mach7/patterns/bindings.hpp>     // Mach7 support for bindings on arbitrary UDT
#include <mach7/patterns/constructor.hpp>  // Support for constructor patterns
#include <mach7/patterns/primitive.hpp>    // Wildcard, variable and value patterns
#include <xtl/adapters/std/memory.hpp>     // XTL subtyping adapters for standard smart pointers

elefthei

Keybase proof

I hereby claim:

• I am elefthei on github.
• I am elefthei (https://keybase.io/elefthei) on keybase.
• I have a public key ASBIMh37Whae5fximDyMoUP_oWYMs_eTlwValKAAU_vcvAo

To claim this, I am signing this object: