Lysxia

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

Lysxia

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

import qualified GHC.Generics as G

Lysxia

{-# LANGUAGE ScopedTypeVariables #-}

import Control.Monad.Cont
import Control.Monad.State
import Control.Monad.Except
import Data.Either
import Data.Foldable
import Data.Set (Set)
import qualified Data.Set as Set

Lysxia

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import GHC.TypeNats

Lysxia

{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-}

import System.Console.Haskeline
import System.IO
import System.IO.Unsafe
import Control.Monad.State.Strict
import Control.Monad.Reader
import qualified Data.ByteString.Char8 as B
import Data.Maybe
import Data.List 

Lysxia

Require Import List.
Import ListNotations.
Open Scope list_scope.

CoInductive stream (a : Type) :=
| scons : a -> stream a -> stream a.

Arguments scons {a}.

Definition repeat {a} (x : a) : stream a :=

Lysxia

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

import Data.Aeson

Lysxia

{-# LANGUAGE DataKinds, GADTs, UndecidableInstances, TypeFamilies #-}

data Nat = Z | S Nat

type family Infinite :: Nat where Infinite = S Infinite

data Vec (n :: Nat) where VZ :: Vec Z ; VS :: Vec n -> Vec (S n)

x :: Vec Infinite
x = VS x

Lysxia

Require Import Nat.

Definition TT (n : nat) : Type := if even n then bool else nat.

Definition bla (n : nat) : TT n.
unfold TT.
destruct (even n).
apply true.
apply 4.
Defined.

Lysxia

CoInductive Tree : Type :=
| Leaf
| Node : Tree -> Tree -> Tree.

Inductive Prefix : Tree -> Type :=
| LeafP : Prefix Leaf
| NodeP : forall {t1 t2}, Prefix t1 -> Prefix t2 -> Prefix (Node t1 t2)
| EmptyP : forall {t}, Prefix t.

Fixpoint prefix_union {t : Tree} (q1 q2 : Prefix t) : Prefix t.