view paper/src/AgdaDebug.agda.replaced @ 2:c7acb9211784

add code, figure. and paper fix content
author ryokka
date Mon, 27 Jan 2020 20:41:36 +0900
parents
children
line wrap: on
line source

open import Level renaming (suc to succ ; zero to Zero )

module AgdaDebug where

open import stack

open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Core
open import Data.Nat
open import Function


open SingleLinkedStack
open Stack

testStack07 : {m : Level } @$\rightarrow$@ Maybe (Element @$\mathbb{N}$@)
testStack07 = pushSingleLinkedStack emptySingleLinkedStack 1 (\s @$\rightarrow$@ pushSingleLinkedStack s 2 (\s @$\rightarrow$@ top s))

testStack08 = pushSingleLinkedStack emptySingleLinkedStack 1
  $ \s @$\rightarrow$@ pushSingleLinkedStack s 2
  $ \s @$\rightarrow$@ pushSingleLinkedStack s 3
  $ \s @$\rightarrow$@ pushSingleLinkedStack s 4
  $ \s @$\rightarrow$@ pushSingleLinkedStack s 5
  $ \s @$\rightarrow$@ top s


testStack10 = pushStack emptySingleLinkedStack 1
  $ \s @$\rightarrow$@ pushStack 2
  $ \s @$\rightarrow$@ pushStack 3
  $ \s @$\rightarrow$@ pushStack 4
  $ \s @$\rightarrow$@ pushStack 5
  $ \s @$\rightarrow$@ top s