<*> + <*> | + pure (\u1 -> (\u2 -> u1)) | ` <*> | + <*> | | + <*> | | | + pure (\u1 -> (\u2 -> u1)) | | | ` pure (\u1 -> u1) | | ` def | | ` <*> | | + <*> | | | + <*> | | | | + pure (\u1 -> (\u2 -> u1)) | | | | ` pure (\u1 -> u1) | | | ` <*> | | | + <*> | | | | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2))) | | | | ` def | | | | ` pure Term | | | ` def | | | ` <|> | | | + <*> | | | | + <*> | | | | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3)))) | | | | | ` <*> | | | | | + <*> | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) | | | | | | ` pure (\u1 -> (\u2 -> u1)) | | | | | ` <|> | | | | | + <*> | | | | | | + <*> | | | | | | | + <*> | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | ` pure (\u1 -> u1) | | | | | | | ` def | | | | | | | ` <*> | | | | | | | + <*> | | | | | | | | + <*> | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | ` satisfy | | | | | | | ` ref | | | | | | ` <*> | | | | | | + <*> | | | | | | | + <*> | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | ` pure (\u1 -> u1) | | | | | | | ` <*> | | | | | | | + <*> | | | | | | | | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2))) | | | | | | | | ` pure Term | | | | | | | ` def | | | | | | | ` <|> | | | | | | | + <*> | | | | | | | | + <*> | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3)))) | | | | | | | | | ` <*> | | | | | | | | | + <*> | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) | | | | | | | | | | ` pure (\u1 -> (\u2 -> u1)) | | | | | | | | | ` ref | | | | | | | | ` rec | | | | | | | ` pure (\u1 -> u1) | | | | | | ` pure Term | | | | | ` <*> | | | | | + <*> | | | | | | + <*> | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | ` pure (\u1 -> u1) | | | | | | ` <*> | | | | | | + <*> | | | | | | | + <*> | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | ` pure (\u1 -> u1) | | | | | | | ` try | | | | | | | ` <*> | | | | | | | + <*> | | | | | | | | + pure cons | | | | | | | | ` <*> | | | | | | | | + <*> | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | ` pure '/' | | | | | | | | ` satisfy | | | | | | | ` <*> | | | | | | | + <*> | | | | | | | | + pure cons | | | | | | | | ` <*> | | | | | | | | + <*> | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | ` pure '/' | | | | | | | | ` satisfy | | | | | | | ` pure Term | | | | | | ` <*> | | | | | | + <*> | | | | | | | + <*> | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | ` pure (\u1 -> u1) | | | | | | | ` <*> | | | | | | | + <*> | | | | | | | | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2))) | | | | | | | | ` ref | | | | | | | ` def | | | | | | | ` <|> | | | | | | | + <*> | | | | | | | | + <*> | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3)))) | | | | | | | | | ` <*> | | | | | | | | | + <*> | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) | | | | | | | | | | ` pure (\u1 -> (\u2 -> u1)) | | | | | | | | | ` satisfy | | | | | | | | ` rec | | | | | | | ` pure (\u1 -> u1) | | | | | | ` ref | | | | | ` ref | | | | ` rec | | | ` pure (\u1 -> u1) | | ` ref | ` <*> | + <*> | | + <*> | | | + pure (\u1 -> (\u2 -> u1)) | | | ` pure (\u1 -> u1) | | ` <*> | | + <*> | | | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2))) | | | ` ref | | ` def | | ` <|> | | + <*> | | | + <*> | | | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3)))) | | | | ` <*> | | | | + <*> | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) | | | | | ` pure (\u1 -> (\u2 -> u1)) | | | | ` <*> | | | | + <*> | | | | | + <*> | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | ` pure (\u1 -> u1) | | | | | ` <*> | | | | | + <*> | | | | | | + <*> | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | ` pure (\u1 -> u1) | | | | | | ` <*> | | | | | | + <*> | | | | | | | + <*> | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | ` pure (\u1 -> u1) | | | | | | | ` <*> | | | | | | | + <*> | | | | | | | | + <*> | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | ` try | | | | | | | | ` <*> | | | | | | | | + <*> | | | | | | | | | + <*> | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | ` try | | | | | | | | | ` <*> | | | | | | | | | + <*> | | | | | | | | | | + pure cons | | | | | | | | | | ` <*> | | | | | | | | | | + <*> | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | ` pure 'f' | | | | | | | | | | ` satisfy | | | | | | | | | ` <*> | | | | | | | | | + <*> | | | | | | | | | | + pure cons | | | | | | | | | | ` <*> | | | | | | | | | | + <*> | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | ` pure 'u' | | | | | | | | | | ` satisfy | | | | | | | | | ` <*> | | | | | | | | | + <*> | | | | | | | | | | + pure cons | | | | | | | | | | ` <*> | | | | | | | | | | + <*> | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | ` pure 'n' | | | | | | | | | | ` satisfy | | | | | | | | | ` <*> | | | | | | | | | + <*> | | | | | | | | | | + pure cons | | | | | | | | | | ` <*> | | | | | | | | | | + <*> | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | ` pure 'c' | | | | | | | | | | ` satisfy | | | | | | | | | ` <*> | | | | | | | | | + <*> | | | | | | | | | | + pure cons | | | | | | | | | | ` <*> | | | | | | | | | | + <*> | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | ` pure 't' | | | | | | | | | | ` satisfy | | | | | | | | | ` <*> | | | | | | | | | + <*> | | | | | | | | | | + pure cons | | | | | | | | | | ` <*> | | | | | | | | | | + <*> | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | ` pure 'i' | | | | | | | | | | ` satisfy | | | | | | | | | ` <*> | | | | | | | | | + <*> | | | | | | | | | | + pure cons | | | | | | | | | | ` <*> | | | | | | | | | | + <*> | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | ` pure 'o' | | | | | | | | | | ` satisfy | | | | | | | | | ` <*> | | | | | | | | | + <*> | | | | | | | | | | + pure cons | | | | | | | | | | ` <*> | | | | | | | | | | + <*> | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | ` pure 'n' | | | | | | | | | | ` satisfy | | | | | | | | | ` def | | | | | | | | | ` pure Term | | | | | | | | ` def | | | | | | | | ` negLook | | | | | | | | ` satisfy | | | | | | | ` ref | | | | | | ` def | | | | | | ` <*> | | | | | | + <*> | | | | | | | + <*> | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | ` pure (\u1 -> u1) | | | | | | | ` try | | | | | | | ` <*> | | | | | | | + <*> | | | | | | | | + <*> | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | ` satisfy | | | | | | | ` <*> | | | | | | | + <*> | | | | | | | | + <*> | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | ` <*> | | | | | | | | + <*> | | | | | | | | | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2))) | | | | | | | | | ` ref | | | | | | | | ` def | | | | | | | | ` <|> | | | | | | | | + <*> | | | | | | | | | + <*> | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3)))) | | | | | | | | | | ` <*> | | | | | | | | | | + <*> | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) | | | | | | | | | | | ` pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | ` satisfy | | | | | | | | | ` rec | | | | | | | | ` pure (\u1 -> u1) | | | | | | | ` ref | | | | | | ` ref | | | | | ` <*> | | | | | + <*> | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | ` <*> | | | | | | + <*> | | | | | | | + <*> | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | ` pure (\u1 -> u1) | | | | | | | ` def | | | | | | | ` <*> | | | | | | | + <*> | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | ` <*> | | | | | | | | + <*> | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | ` pure '(' | | | | | | | | ` satisfy | | | | | | | ` ref | | | | | | ` <*> | | | | | | + <*> | | | | | | | + <*> | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | ` pure (\u1 -> u1) | | | | | | | ` def | | | | | | | ` <|> | | | | | | | + <*> | | | | | | | | + <*> | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | ` pure Term | | | | | | | | ` <*> | | | | | | | | + <*> | | | | | | | | | + <*> | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | ` def | | | | | | | | | ` <*> | | | | | | | | | + <*> | | | | | | | | | | + <*> | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | ` ref | | | | | | | | | ` <|> | | | | | | | | | + <*> | | | | | | | | | | + <*> | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | ` pure Term | | | | | | | | | | ` def | | | | | | | | | | ` <*> | | | | | | | | | | + <*> | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | ` <*> | | | | | | | | | | | + <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | ` <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | ` pure '[' | | | | | | | | | | | | | ` satisfy | | | | | | | | | | | | ` ref | | | | | | | | | | | ` <*> | | | | | | | | | | | + <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | ` def | | | | | | | | | | | | ` satisfy | | | | | | | | | | | ` <*> | | | | | | | | | | | + <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | ` <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2))) | | | | | | | | | | | | | ` pure Term | | | | | | | | | | | | ` def | | | | | | | | | | | | ` <|> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3)))) | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) | | | | | | | | | | | | | | | ` pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | ` rec | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | ` pure Term | | | | | | | | | | ` <*> | | | | | | | | | | + <*> | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | ` <*> | | | | | | | | | | | + <*> | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | ` pure ']' | | | | | | | | | | | ` satisfy | | | | | | | | | | ` ref | | | | | | | | | ` ref | | | | | | | | ` <*> | | | | | | | | + <*> | | | | | | | | | + <*> | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | ` <*> | | | | | | | | | + <*> | | | | | | | | | | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2))) | | | | | | | | | | ` ref | | | | | | | | | ` def | | | | | | | | | ` <|> | | | | | | | | | + <*> | | | | | | | | | | + <*> | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3)))) | | | | | | | | | | | ` <*> | | | | | | | | | | | + def | | | | | | | | | | | | ` <*> | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) | | | | | | | | | | | | ` pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | ` <*> | | | | | | | | | | | + <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | ` def | | | | | | | | | | | | ` <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | ` pure ',' | | | | | | | | | | | | | ` satisfy | | | | | | | | | | | | ` ref | | | | | | | | | | | ` ref | | | | | | | | | | ` rec | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | ` ref | | | | | | | ` ref | | | | | | ` <|> | | | | | | + <*> | | | | | | | + <*> | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | ` pure Term | | | | | | | ` <*> | | | | | | | + <*> | | | | | | | | + <*> | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | ` <*> | | | | | | | | + <*> | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | ` <*> | | | | | | | | | + <*> | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | ` pure ':' | | | | | | | | | ` satisfy | | | | | | | | ` ref | | | | | | | ` ref | | | | | | ` ref | | | | | ` def | | | | | ` <*> | | | | | + <*> | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | ` <*> | | | | | | + <*> | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | ` pure ')' | | | | | | ` satisfy | | | | | ` ref | | | | ` def | | | | ` <*> | | | | + <*> | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | ` <*> | | | | | + <*> | | | | | | + <*> | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | ` pure (\u1 -> u1) | | | | | | ` <*> | | | | | | + <*> | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | ` <*> | | | | | | | + <*> | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | ` pure '{' | | | | | | | ` satisfy | | | | | | ` ref | | | | | ` <*> | | | | | + <*> | | | | | | + <*> | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | ` pure (\u1 -> u1) | | | | | | ` <*> | | | | | | + <*> | | | | | | | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2))) | | | | | | | ` ref | | | | | | ` def | | | | | | ` <|> | | | | | | + <*> | | | | | | | + <*> | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3)))) | | | | | | | | ` <*> | | | | | | | | + <*> | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) | | | | | | | | | ` pure (\u1 -> (\u2 -> u1)) | | | | | | | | ` <|> | | | | | | | | + <|> | | | | | | | | | + <|> | | | | | | | | | | + <*> | | | | | | | | | | | + <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | ` <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | | | ` try | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | | | | ` try | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + pure cons | | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | | ` pure 'i' | | | | | | | | | | | | | | | | | ` satisfy | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + pure cons | | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | | ` pure 'f' | | | | | | | | | | | | | | | | | ` satisfy | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | ` def | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | | ` def | | | | | | | | | | | | | | ` <|> | | | | | | | | | | | | | | + <|> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | | | | | ` <|> | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | | | ` pure '0' | | | | | | | | | | | | | | | | | | ` satisfy | | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | | ` pure '1' | | | | | | | | | | | | | | | | | ` satisfy | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | | ` pure '\'' | | | | | | | | | | | | | | | | | ` satisfy | | | | | | | | | | | | | | | | ` <|> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | | | | | | ` satisfy | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | | ` pure '\\' | | | | | | | | | | | | | | | | | ` satisfy | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | | | | | ` satisfy | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | ` pure '\'' | | | | | | | | | | | | | | | | ` satisfy | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | ` <|> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | ` pure Term | | | | | | | | | | | | | | | ` <|> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | ` <|> | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | | | ` pure Term | | | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | | | | | | | ` rec | | | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2))) | | | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | | | ` def | | | | | | | | | | | | | | | | | | | ` <|> | | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3)))) | | | | | | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | | | | | | + ref | | | | | | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | | | | | ` rec | | | | | | | | | | | | | | | | | | | | ` rec | | | | | | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2))) | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | ` def | | | | | | | | | | | | | | ` <|> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3)))) | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) | | | | | | | | | | | | | | | | | ` pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | | | ` pure '!' | | | | | | | | | | | | | | | | | | ` satisfy | | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | ` rec | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | ` ref | | | | | | | | | | | | ` rec | | | | | | | | | | | ` <|> | | | | | | | | | | | + <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | ` pure Term | | | | | | | | | | | | ` <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | | ` try | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | | | ` try | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + pure cons | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | ` pure 'e' | | | | | | | | | | | | | | | | ` satisfy | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + pure cons | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | ` pure 'l' | | | | | | | | | | | | | | | | ` satisfy | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + pure cons | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | ` pure 's' | | | | | | | | | | | | | | | | ` satisfy | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + pure cons | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | ` pure 'e' | | | | | | | | | | | | | | | | ` satisfy | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | ` ref | | | | | | | | | | | | ` rec | | | | | | | | | | | ` ref | | | | | | | | | | ` <*> | | | | | | | | | | + <*> | | | | | | | | | | | + <*> | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | ` <*> | | | | | | | | | | | + <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | ` <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | ` try | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | | ` try | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + pure cons | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | ` pure 'w' | | | | | | | | | | | | | | | ` satisfy | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + pure cons | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | ` pure 'h' | | | | | | | | | | | | | | | ` satisfy | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + pure cons | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | ` pure 'i' | | | | | | | | | | | | | | | ` satisfy | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + pure cons | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | ` pure 'l' | | | | | | | | | | | | | | | ` satisfy | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + pure cons | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | ` pure 'e' | | | | | | | | | | | | | | | ` satisfy | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | ` ref | | | | | | | | | | | | ` ref | | | | | | | | | | | ` ref | | | | | | | | | | ` rec | | | | | | | | | ` try | | | | | | | | | ` <*> | | | | | | | | | + <*> | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | ` <*> | | | | | | | | | | + <*> | | | | | | | | | | | + <*> | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | ` <*> | | | | | | | | | | | + <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | ` <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | ` <|> | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | ` pure Term | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | | | ` try | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | | | | ` try | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + pure cons | | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | | ` pure 'v' | | | | | | | | | | | | | | | | | ` satisfy | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + pure cons | | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | | ` pure 'a' | | | | | | | | | | | | | | | | | ` satisfy | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + pure cons | | | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | | ` pure 'r' | | | | | | | | | | | | | | | | | ` satisfy | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | ` ref | | | | | | | | | | | | ` <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | ` ref | | | | | | | | | | | | ` <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2))) | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | ` def | | | | | | | | | | | | | ` <|> | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3)))) | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | + ref | | | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | | ` rec | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | ` ref | | | | | | | | | | | ` <*> | | | | | | | | | | | + <*> | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | ` <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | ` pure '=' | | | | | | | | | | | | ` satisfy | | | | | | | | | | | ` ref | | | | | | | | | | ` <*> | | | | | | | | | | + <*> | | | | | | | | | | | + <*> | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | ` ref | | | | | | | | | | ` <*> | | | | | | | | | | + <*> | | | | | | | | | | | + <*> | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | ` <*> | | | | | | | | | | | + <*> | | | | | | | | | | | | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2))) | | | | | | | | | | | | ` ref | | | | | | | | | | | ` def | | | | | | | | | | | ` <|> | | | | | | | | | | | + <*> | | | | | | | | | | | | + <*> | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3)))) | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | + ref | | | | | | | | | | | | | ` <*> | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | + <*> | | | | | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | | | | | ` ref | | | | | | | | | | | | | ` ref | | | | | | | | | | | | ` rec | | | | | | | | | | | ` pure (\u1 -> u1) | | | | | | | | | | ` ref | | | | | | | | | ` def | | | | | | | | | ` <*> | | | | | | | | | + <*> | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | ` <*> | | | | | | | | | | + <*> | | | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | | | ` pure ';' | | | | | | | | | | ` satisfy | | | | | | | | | ` ref | | | | | | | | ` <*> | | | | | | | | + <*> | | | | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | | | | ` ref | | | | | | | | ` ref | | | | | | | ` rec | | | | | | ` pure (\u1 -> u1) | | | | | ` ref | | | | ` <*> | | | | + <*> | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | ` <*> | | | | | + <*> | | | | | | + pure (\u1 -> (\u2 -> u1)) | | | | | | ` pure '}' | | | | | ` satisfy | | | | ` ref | | | ` rec | | ` pure (\u1 -> u1) | ` ref ` eof