[−] List of all items
Structs
- agda::AgdaRead
- agda::JustStdio
- agda::ProcessStdio
- agda::ReplState
- cmd::GoalInput
- cmd::IOTCM
- cmd::InputWithRewrite
- pos::InteractionPoint
- pos::Interval
- pos::Pos
- resp::AgdaError
- resp::AllGoalsWarnings
- resp::AspectHighlight
- resp::CmpSomething
- resp::CommandState
- resp::Context
- resp::DefinitionSite
- resp::FindInstanceCandidate
- resp::FindInstanceOF
- resp::GiveAction
- resp::GiveResult
- resp::GoalSpecific
- resp::GoalType
- resp::Highlighting
- resp::HighlightingInfo
- resp::InferredType
- resp::JustSomething
- resp::MakeCase
- resp::ModuleContents
- resp::NamedPrettyTCM
- resp::NormalForm
- resp::OfType
- resp::OneSolution
- resp::OutputForm
- resp::PostponedCheckArgs
- resp::ResponseContextEntry
- resp::Status
- resp::TelescopicItem
- resp::TypedAssign
Enums
- base::Cohesion
- base::CompareDirection
- base::Comparison
- base::ComputeMode
- base::Hiding
- base::Polarity
- base::Relevance
- base::Remove
- base::Rewrite
- base::TokenBased
- base::UseForce
- cmd::Cmd
- cmd::HighlightingLevel
- cmd::HighlightingMethod
- hs::HaskellBool
- pos::AgdaRange
- resp::DisplayInfo
- resp::GoalInfo
- resp::GoalTypeAux
- resp::MakeCaseVariant
- resp::OutputConstraint
- resp::Resp
Traits
Functions
- agda::deserialize_agda
- agda::init_agda_process
- agda::load_file
- agda::preprint_agda_result
- agda::send_command
- agda::start_agda
- agda::verify::check_version
- debug::debug_command_via
- debug::debug_response_via
- debug::dont_debug_command
- debug::dont_debug_response
- debug::toggle_debug_command
- debug::toggle_debug_response
Typedefs
- agda::AgdaResult
- agda::NextResult
- pos::IntPos
- pos::InteractionId
- pos::ProblemId
- resp::InvisibleGoal
- resp::VisibleGoal