rzk-0.5.1: An experimental proof assistant for synthetic ∞-categories

Safe Haskell	Safe-Inferred
Language	Haskell2010

Language.Rzk.Syntax

Synopsis

module Language.Rzk.Syntax.Abs
parseModule :: String -> Either String Module
parseModuleRzk :: String -> Either String Module
parseModuleFile :: FilePath -> IO (Either String Module)
parseTerm :: String -> Either String Term
printTree :: Print a => a -> String
tryExtractMarkdownCodeBlocks :: String -> String -> String
extractMarkdownCodeBlocks :: String -> String -> String

Documentation

module Language.Rzk.Syntax.Abs

parseModule :: String -> Either String Module Source #

parseModuleRzk :: String -> Either String Module Source #

parseModuleFile :: FilePath -> IO (Either String Module) Source #

parseTerm :: String -> Either String Term Source #

printTree :: Print a => a -> String Source #

The top-level printing method.

tryExtractMarkdownCodeBlocks :: String -> String -> String Source #

extractMarkdownCodeBlocks :: String -> String -> String Source #

Extract rzk code from a Markdown file

>>> putStrLn $ detectMarkdownCodeBlocks "\n```rzk\n#lang rzk-1\n```\nasd asd\n```rzk\n#def x : U\n  := U\n``` asda"
#lang rzk-1
#def x : U
  := U