<*> + <*> | + <*> | | + <*> | | | + <*> | | | | + pure (\u1 -> (\u2 -> (\u3 -> (\u4 -> (\u5 -> u4))))) | | | | ` <*> | | | | + <*> | | | | | + <*> | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> u3))) | | | | | | ` pure Term | | | | | ` <|> | | | | | + <*> | | | | | | + <*> | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> u2 u3))) | | | | | | | ` <|> | | | | | | | + <*> | | | | | | | | + <*> | | | | | | | | | + pure (\u1 -> (\u2 -> Term)) | | | | | | | | | ` <*> | | | | | | | | | + <*> | | | | | | | | | | + pure (\u1 -> (\u2 -> u2)) | | | | | | | | | | ` def | | | | | | | | | | ` satisfy | | | | | | | | | ` ref | | | | | | | | ` <|> | | | | | | | | + <*> | | | | | | | | | + <*> | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> u2 u3))) | | | | | | | | | | ` ref | | | | | | | | | ` rec | | | | | | | | ` pure (\u1 -> u1) | | | | | | | ` <*> | | | | | | | + <*> | | | | | | | | + <*> | | | | | | | | | + <*> | | | | | | | | | | + <*> | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (\u4 -> (\u5 -> u5))))) | | | | | | | | | | | ` try | | | | | | | | | | | ` <*> | | | | | | | | | | | + <*> | | | | | | | | | | | | + pure (\u1 -> (\u2 -> '/' : ('/' : Term))) | | | | | | | | | | | | ` ref | | | | | | | | | | | ` ref | | | | | | | | | | ` ref | | | | | | | | | ` <|> | | | | | | | | | + <*> | | | | | | | | | | + <*> | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> u2 u3))) | | | | | | | | | | | ` ref | | | | | | | | | | ` rec | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | ` ref | | | | | | | ` ref | | | | | | ` rec | | | | | ` pure (\u1 -> u1) | | | | ` ref | | | ` ref | | ` <|> | | + <*> | | | + <*> | | | | + <*> | | | | | + <*> | | | | | | + <*> | | | | | | | + <*> | | | | | | | | + <*> | | | | | | | | | + <*> | | | | | | | | | | + <*> | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (\u4 -> (\u5 -> (\u6 -> (\u7 -> (\u8 -> (\u9 -> (\u10 -> u9 u10)))))))))) | | | | | | | | | | | ` try | | | | | | | | | | | ` <*> | | | | | | | | | | | + <*> | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u2)) | | | | | | | | | | | | ` try | | | | | | | | | | | | ` <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (\u4 -> (\u5 -> (\u6 -> (\u7 -> (\u8 -> (\u9 -> 'f' : ('u' : ('n' : ('c' : ('t' : ('i' : ('o' : ('n' : u9)))))))))))))))) | | | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | ` ref | | | | | | | | | | | | ` pure Term | | | | | | | | | | | ` negLook | | | | | | | | | | | ` ref | | | | | | | | | | ` ref | | | | | | | | | ` <*> | | | | | | | | | + <*> | | | | | | | | | | + pure (\u1 -> (\u2 -> u2)) | | | | | | | | | | ` try | | | | | | | | | | ` <*> | | | | | | | | | | + <*> | | | | | | | | | | | + <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (\u4 -> u4)))) | | | | | | | | | | | | | ` ref | | | | | | | | | | | | ` ref | | | | | | | | | | | ` <|> | | | | | | | | | | | + <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> u2 u3))) | | | | | | | | | | | | | ` ref | | | | | | | | | | | | ` rec | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | ` ref | | | | | | | | | ` ref | | | | | | | | ` <*> | | | | | | | | + <*> | | | | | | | | | + pure (\u1 -> (\u2 -> '(')) | | | | | | | | | ` ref | | | | | | | | ` ref | | | | | | | ` <|> | | | | | | | + <*> | | | | | | | | + <*> | | | | | | | | | + <*> | | | | | | | | | | + <*> | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (\u4 -> Term)))) | | | | | | | | | | | ` <*> | | | | | | | | | | | + <*> | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u2)) | | | | | | | | | | | | ` ref | | | | | | | | | | | ` <|> | | | | | | | | | | | + <*> | | | | | | | | | | | | + pure (\u1 -> Term) | | | | | | | | | | | | ` <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (\u4 -> (\u5 -> (\u6 -> Term)))))) | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | ` <|> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> u2 u3))) | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | ` rec | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | ` ref | | | | | | | | | | | | ` ref | | | | | | | | | | | ` ref | | | | | | | | | | ` ref | | | | | | | | | ` <|> | | | | | | | | | + <*> | | | | | | | | | | + <*> | | | | | | | | | | | + <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (\u4 -> (\u5 -> (u1 u3) (u4 u5)))))) | | | | | | | | | | | | | ` pure (\u1 -> (\u2 -> u2)) | | | | | | | | | | | | ` <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> ',')) | | | | | | | | | | | | | ` ref | | | | | | | | | | | | ` ref | | | | | | | | | | | ` ref | | | | | | | | | | ` rec | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | ` ref | | | | | | | ` ref | | | | | | ` <|> | | | | | | + <*> | | | | | | | + <*> | | | | | | | | + <*> | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> Term))) | | | | | | | | | ` ref | | | | | | | | ` ref | | | | | | | ` ref | | | | | | ` ref | | | | | ` <*> | | | | | + <*> | | | | | | + pure (\u1 -> (\u2 -> ')')) | | | | | | ` ref | | | | | ` ref | | | | ` <*> | | | | + <*> | | | | | + <*> | | | | | | + <*> | | | | | | | + <*> | | | | | | | | + <*> | | | | | | | | | + <*> | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (\u4 -> (\u5 -> (\u6 -> (\u7 -> u5))))))) | | | | | | | | | | ` ref | | | | | | | | | ` ref | | | | | | | | ` ref | | | | | | | ` <|> | | | | | | | + <*> | | | | | | | | + <*> | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> u2 u3))) | | | | | | | | | ` <|> | | | | | | | | | + <*> | | | | | | | | | | + <*> | | | | | | | | | | | + <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (\u4 -> (\u5 -> u5))))) | | | | | | | | | | | | | | ` try | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u2)) | | | | | | | | | | | | | | | ` try | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> 'i' : ('f' : u3)))) | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | ` ref | | | | | | | | | | | | ` <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (\u4 -> u4)))) | | | | | | | | | | | | | | | ` <|> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u2)) | | | | | | | | | | | | | | | | | ` <|> | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | + pure (\u1 -> '0') | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | | + pure (\u1 -> '1') | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | ` <|> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (\u4 -> u2)))) | | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | | ` <|> | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u2)) | | | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> u3))) | | | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u2)) | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | ` <|> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + pure (\u1 -> Term) | | | | | | | | | | | | | | | | ` <|> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> u2))) | | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | | ` <|> | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (\u4 -> Term)))) | | | | | | | | | | | | | | | | | | | | | | ` rec | | | | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | | | | ` <|> | | | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (\u4 -> (\u5 -> (u1 u3) (u4 u5)))))) | | | | | | | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | | | | | | ` rec | | | | | | | | | | | | | | | | | | | | | ` rec | | | | | | | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | ` <|> | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (\u4 -> (\u5 -> u4 u5))))) | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | ` rec | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | ` ref | | | | | | | | | | | ` rec | | | | | | | | | | ` <|> | | | | | | | | | | + <*> | | | | | | | | | | | + <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> Term))) | | | | | | | | | | | | | ` try | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u2)) | | | | | | | | | | | | | | ` try | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (\u4 -> (\u5 -> 'e' : ('l' : ('s' : ('e' : u5)))))))) | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | ` ref | | | | | | | | | | | | ` ref | | | | | | | | | | | ` rec | | | | | | | | | | ` ref | | | | | | | | | ` <|> | | | | | | | | | + <*> | | | | | | | | | | + <*> | | | | | | | | | | | + <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (\u4 -> u4)))) | | | | | | | | | | | | | ` try | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u2)) | | | | | | | | | | | | | | ` try | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (\u4 -> (\u5 -> (\u6 -> 'w' : ('h' : ('i' : ('l' : ('e' : u6)))))))))) | | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | ` ref | | | | | | | | | | | | ` ref | | | | | | | | | | | ` ref | | | | | | | | | | ` rec | | | | | | | | | ` <|> | | | | | | | | | + try | | | | | | | | | | ` <*> | | | | | | | | | | + <*> | | | | | | | | | | | + <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (\u4 -> (\u5 -> (\u6 -> (\u7 -> (\u8 -> (\u9 -> (\u10 -> (\u11 -> (\u12 -> u11)))))))))))) | | | | | | | | | | | | | | | | | | | | | ` <|> | | | | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> Term)) | | | | | | | | | | | | | | | | | | | | | | | ` try | | | | | | | | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u2)) | | | | | | | | | | | | | | | | | | | | | | | | ` try | | | | | | | | | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (\u4 -> 'v' : ('a' : ('r' : u4)))))) | | | | | | | | | | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | | ` <|> | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (\u4 -> (\u5 -> (u1 u3) (u4 u5)))))) | | | | | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | | | ` rec | | | | | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | ` ref | | | | | | | | | | | | ` <|> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (\u4 -> (\u5 -> (u1 u3) (u4 u5)))))) | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | ` rec | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | ` ref | | | | | | | | | | ` <*> | | | | | | | | | | + <*> | | | | | | | | | | | + pure (\u1 -> (\u2 -> ';')) | | | | | | | | | | | ` ref | | | | | | | | | | ` ref | | | | | | | | | ` <*> | | | | | | | | | + <*> | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | ` ref | | | | | | | | | ` ref | | | | | | | | ` rec | | | | | | | ` pure (\u1 -> u1) | | | | | | ` ref | | | | | ` ref | | | | ` ref | | | ` rec | | ` pure (\u1 -> u1) | ` ref ` eof