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

bond15

module Multiverse where 


module types where 
    open import Data.Nat 
    open import Data.String 
    open import Data.Bool 
    open import Data.Product

    data Type₁ : Set where 

bond15

module foo where 
    data ⊘ : Set where
    data ⊤ : Set where tt : ⊤
    open import Cubical.Data.Bool
    open import Cubical.Foundations.Isomorphism  
    open import Cubical.Foundations.Prelude 
 
    postulate 
        f : Set → Bool
        reduction₁ : f (⊤ × ⊤) ≡ true