Mercurial > hg > Papers > 2018 > ryokka-thesis

view final_main/src/AgdaTreeDebugReturnNode4.agda @ 3:2155c6ff589f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix Section, Capter, and Mindmap. add some Code
author ryokka
date Fri, 16 Feb 2018 16:58:40 +0900
parents
children
line wrap: on
line source

test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1
$ \t -> putTree1 t 2 2
$ \t -> putTree1 t 3 3
$ \t -> putTree1 t 4 4
$ \t -> getRedBlackTree t 4
$ \t x -> x

-- C-c C-n test31 return
  -- Just
  -- (record
  -- { key = 4
  -- ; value = 4
  -- ; right = Nothing
  -- ; left = Nothing
  -- ; color = Red
  -- })