Joshiryoku.agda

module Joshiryoku where

infix 1 >_< ^_^ ・_・
infix 2 （_） [_]
infix 3 o_o ∩_∩ ☜_☞

data Mouse : Set where
    O : Mouse
    - : Mouse
    ω : Mouse
    益 : Mouse

data Eyes : Set where
    >< : Eyes
    >_< : Mouse -> Eyes

    ^^ : Eyes
    ^_^ : Mouse -> Eyes

    ・・ : Eyes
    ・_・ : Mouse -> Eyes

    ◔ิ◔ิ : Eyes

    ◞≼◉ื≽◟_◞≼◉ื≽◟ :  Mouse -> Eyes

data Rinkaku : Set where
    （_） : Eyes -> Rinkaku    
    [_] : Eyes -> Rinkaku

data Hand : Set where
    o_o : Rinkaku -> Hand

    ∩_∩ : Rinkaku -> Hand

    ☜_☞ : Rinkaku -> Hand

hoge : Eyes
hoge = > O <

piyo : Rinkaku
piyo = [ ・ ω ・ ]

fuga : Hand
fuga = o （ ^ - ^ ） o

poyoyo : Eyes
poyoyo = (◞≼◉ื≽◟ 益 ◞≼◉ื≽◟)

nyo- : Hand
nyo- = ☜ （ ◔ิ◔ิ ） ☞