bond15

open import Cubical.Data.Bool
open import Cubical.Data.Unit
open import Cubical.Foundations.Prelude
open import Cubical.Data.Sigma
open import Cubical.Data.Sum
open import Cubical.Foundations.HLevels
open import Cubical.Functions.Logic
open import Cubical.Foundations.Structure
open import Cubical.HITs.PropositionalTruncation 

bond15

module src.sandbox where 
    open import Cubical.Data.Sigma
    open import Cubical.Data.Bool

    record Monad (F : Set → Set) : Set₁ where 
        field
            return : ∀ {A} → A → F A
            _>>=_ : ∀{A B} → F A → (A → F B) → F B
        
        _>>_ : ∀{A B} → F A → F B → F B

bond15

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

    open import Cubical.Data.Unit renaming (Unit to ⊤)
    open import Cubical.Data.Sigma
    open import Cubical.Foundations.Prelude 


    _∘_ : {A B C : Set₀} → (B → C) → (A → B) → A → C 
    g ∘ f = λ a → g (f a)

bond15

theory hw 
  imports Main
begin

datatype variable = A | B | C | D | Z

(* a literal is a variable or its negation*)
datatype literal = Not variable | Id variable

(* given an assignment of variables to truth values, we can evaluate a literal to a truth value*)

bond15

#define DEBUG
#ifdef DEBUG
# define PRINT(x) errs() << x;
#else
# define PRINT(x) {};
#endif

bond15

import List
import Maybe

data Parser (a : Type) = Parser (String → List (a , String))

parse : ∀ {a : Type}. Parser a → String → List (a , String)
parse (Parser p) = p

result : ∀{a : Type}. a → Parser a 
result a = Parser (λs → Next (a,s) Empty)

bond15

In Granule (the base calculus is linear) these two tests violate linearity:

data Foo a = Bar a

test1 : Foo Int -> (Int , Int)
test1 (Bar mustUseOnce) = (mustUseOnce, mustUseOnce)

test2 : Foo Int -> Int
test2 (Bar mustUseOnce) = 42

bond15

Module Type AT.
Parameter x : nat.
End AT.

Module A (Import a : AT).
Include a.
Definition y := a.x.

End A.
Print A.

bond15

    data S₁ : Set where 
        base : S₁
        loop : base ≡ base

    _ : S₁ 
    _ = base 

    _ : S₁ 
    _ = loop i0

bond15

record Poly : Set₁ where
  constructor _◂_◂_ 
  field
    pos : Set
    dir : pos → Set
    α : (p : pos)(d : dir p) → Set

open import Data.Product
 
_⇒_ : Poly → Poly → Poly