Strings

Content created by Fredrik Bakke, Fernando Chu and Egbert Rijke.

Created on 2023-04-27.
Last modified on 2023-10-21.

module primitives.strings where
Imports
open import elementary-number-theory.natural-numbers

open import foundation.booleans
open import foundation.dependent-pair-types
open import foundation.maybe
open import foundation.universe-levels

open import lists.lists

open import primitives.characters

Idea

The String type represents strings. Agda provides primitive functions to manipulate them. Strings are written between double quotes, e.g. "agda-unimath".

Definitions

postulate
  String : UU lzero

{-# BUILTIN STRING String #-}

primitive
  primStringUncons : String  Maybe' (Σ Char  _  String))
  primStringToList : String  list Char
  primStringFromList : list Char  String
  primStringAppend : String  String  String
  primStringEquality : String  String  bool
  primShowChar : Char  String
  primShowString : String  String
  primShowNat :   String

Recent changes