mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-05-22 17:42:51 -06:00
Split widesnake example. Changed examples to use rec and sig keywords.
This commit is contained in:
@@ -1,5 +1,3 @@
|
||||
import bool
|
||||
|
||||
data Cat : Type where {
|
||||
CN : Cat ;
|
||||
NP : Cat ;
|
||||
@@ -207,17 +205,3 @@ data Tree : (_ : Cat)-> Type where {
|
||||
|
||||
derive composOp Tree
|
||||
derive composFold Tree
|
||||
|
||||
monoid_Bool = { zero = False; plus = \x -> \y -> x && y }
|
||||
|
||||
isSnake : (A : Tree) -> Tree A -> Bool
|
||||
isSnake _ x = case x of
|
||||
Snake -> True
|
||||
_ -> composFold_Tree Bool monoid_Bool ? isSnake x
|
||||
|
||||
wideSnake : (A : Cat) -> Tree A -> Tree A
|
||||
wideSnake _ x = case x of
|
||||
Wide y -> let y' : CN = wideSnake ? y
|
||||
in if isSnake CN y' then Thick y' else Wide y'
|
||||
_ -> composOp_Tree ? wideSnake x
|
||||
|
||||
|
||||
Reference in New Issue
Block a user