Agda-2.2.6: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
Agda.Interaction.CommandLine.CommandLine
Synopsis
data
ExitCode
a
=
Continue
|
ContinueIn
TCEnv
|
Return
a
type
Command
a = (
String
, [
String
] ->
TCM
(
ExitCode
a))
matchCommand
::
String
-> [
Command
a] ->
Either
[
String
] ([
String
] ->
TCM
(
ExitCode
a))
interaction
::
String
-> [
Command
a] -> (
String
->
TCM
(
ExitCode
a)) ->
IM
a
interactionLoop
::
TCM
(
Maybe
Interface
) ->
IM
()
continueAfter
::
TCM
a ->
TCM
(
ExitCode
b)
loadFile
::
TCM
()
-> [
String
] ->
TCM
()
showConstraints
:: [
String
] ->
TCM
()
showMetas
:: [
String
] ->
TCM
()
showScope
::
TCM
()
metaParseExpr
::
InteractionId
->
String
->
TCM
Expr
actOnMeta
:: [
String
] -> (
InteractionId
->
Expr
->
TCM
a) ->
TCM
a
giveMeta
:: [
String
] ->
TCM
()
refineMeta
:: [
String
] ->
TCM
()
retryConstraints
::
TCM
()
evalIn
:: [
String
] ->
TCM
()
parseExpr
::
String
->
TCM
Expr
evalTerm
::
String
->
TCM
(
ExitCode
a)
typeOf
:: [
String
] ->
TCM
()
typeIn
:: [
String
] ->
TCM
()
showContext
:: [
String
] ->
TCM
()
splashScreen
::
String
help
:: [
Command
a] ->
IO
()
Documentation
data
ExitCode
a
Source
Constructors
Continue
ContinueIn
TCEnv
Return
a
type
Command
a = (
String
, [
String
] ->
TCM
(
ExitCode
a))
Source
matchCommand
::
String
-> [
Command
a] ->
Either
[
String
] ([
String
] ->
TCM
(
ExitCode
a))
Source
interaction
::
String
-> [
Command
a] -> (
String
->
TCM
(
ExitCode
a)) ->
IM
a
Source
interactionLoop
::
TCM
(
Maybe
Interface
) ->
IM
()
Source
The interaction loop.
continueAfter
::
TCM
a ->
TCM
(
ExitCode
b)
Source
loadFile
::
TCM
()
-> [
String
] ->
TCM
()
Source
showConstraints
:: [
String
] ->
TCM
()
Source
showMetas
:: [
String
] ->
TCM
()
Source
showScope
::
TCM
()
Source
metaParseExpr
::
InteractionId
->
String
->
TCM
Expr
Source
actOnMeta
:: [
String
] -> (
InteractionId
->
Expr
->
TCM
a) ->
TCM
a
Source
giveMeta
:: [
String
] ->
TCM
()
Source
refineMeta
:: [
String
] ->
TCM
()
Source
retryConstraints
::
TCM
()
Source
evalIn
:: [
String
] ->
TCM
()
Source
parseExpr
::
String
->
TCM
Expr
Source
evalTerm
::
String
->
TCM
(
ExitCode
a)
Source
typeOf
:: [
String
] ->
TCM
()
Source
typeIn
:: [
String
] ->
TCM
()
Source
showContext
:: [
String
] ->
TCM
()
Source
splashScreen
::
String
Source
The logo that prints when Agda is started in interactive mode.
help
:: [
Command
a] ->
IO
()
Source
The help message
Produced by
Haddock
version 2.4.2