Как соединить строки в Agda

Question

Я пытаюсь соединить строки на языке agda.Мой код до сих пор

open import Common.IO
open import Common.String


f  : String  → String
f  x  =  x



main = putStrLn (f  "Hello, world!")

как я могу присоединиться к строкам.В ruby ​​это будет

open import Common.IO
open import Common.String

f  : String  → String
f  x  =  x + ' second string'

main = putStrLn (f  "Hello, world!")

Как мне заставить agda распечатать 'Hello, world!вторая строка '?

Буду очень признателен за рабочий код

Answer 1

Agda имеет примитив primStringAppend, который определен во встроенном модуле Agda.Builtin.String.Например, вы можете написать следующее:

open import Agda.Builtin.String renaming (primStringAppend to _+_)

f  : String  → String
f  x  =  x + " second string"

В зависимости от используемой вами библиотеки, она также может содержать более удобный псевдоним для primStringAppend.