[−] List of all items
Structs
- check::monad::MetaContext
- check::monad::TCS
- check::monad::meta::MetaContext
- check::monad::state::Indentation
- check::monad::state::TCS
- check::pats::Blocked
- check::pats::block::Blocked
- check::rules::clause::eqs::AsBind
- check::rules::clause::eqs::Equation
- check::rules::clause::eqs::PatClass
- check::rules::clause::lhs::Lhs
- check::rules::clause::state::LhsState
- check::rules::clause::state::Problem
- syntax::abs::AbsClause
- syntax::abs::AbsCodataInfo
- syntax::abs::AbsConsInfo
- syntax::abs::AbsDataInfo
- syntax::abs::AbsDefnInfo
- syntax::abs::AbsProjInfo
- syntax::abs::AppView
- syntax::abs::ast::AppView
- syntax::abs::decl::AbsClause
- syntax::abs::decl::AbsCodataInfo
- syntax::abs::decl::AbsConsInfo
- syntax::abs::decl::AbsDataInfo
- syntax::abs::decl::AbsDefnInfo
- syntax::abs::decl::AbsProjInfo
- syntax::abs::desugar::DesugarState
- syntax::abs::desugar::monad::DesugarState
- syntax::common::Bind
- syntax::common::ConHead
- syntax::common::Let
- syntax::core::Clause
- syntax::core::CodataInfo
- syntax::core::ConsInfo
- syntax::core::DataInfo
- syntax::core::FuncInfo
- syntax::core::TermInfo
- syntax::core::ValData
- syntax::core::ast::ValData
- syntax::core::decl::Clause
- syntax::core::decl::CodataInfo
- syntax::core::decl::ConsInfo
- syntax::core::decl::DataInfo
- syntax::core::decl::FuncInfo
- syntax::surf::NamedTele
- syntax::surf::Param
- syntax::surf::ast::NamedTele
- syntax::surf::ast::Param
- syntax::surf::parse::NarcParser
Enums
- check::monad::MetaSol
- check::monad::TCE
- check::monad::error::TCE
- check::monad::meta::MetaSol
- check::pats::Match
- check::pats::Simpl
- check::pats::Stuck
- check::pats::block::Stuck
- check::pats::mat::Match
- syntax::abs::Abs
- syntax::abs::AbsDecl
- syntax::abs::ast::Abs
- syntax::abs::decl::AbsDecl
- syntax::abs::desugar::error::DesugarErr
- syntax::common::Ductive
- syntax::core::Closure
- syntax::core::Decl
- syntax::core::Elim
- syntax::core::Term
- syntax::core::Val
- syntax::core::ast::Closure
- syntax::core::ast::Elim
- syntax::core::ast::Term
- syntax::core::ast::Val
- syntax::core::decl::Decl
- syntax::core::subst::PrimSubst
- syntax::core::subst::prim::PrimSubst
- syntax::pat::Copat
- syntax::pat::Pat
- syntax::surf::Expr
- syntax::surf::ExprDecl
- syntax::surf::Rule
- syntax::surf::ast::Expr
- syntax::surf::ast::ExprDecl
- syntax::surf::parse::Rule
Traits
- check::rules::term::meta::HasMeta
- check::rules::term::unify::Unify
- syntax::core::FoldVal
- syntax::core::ast_fold::FoldVal
- syntax::core::subst::DeBruijn
- syntax::core::subst::RedEx
- syntax::core::subst::dbi::DeBruijn
- syntax::core::subst::redex::RedEx
- syntax::pat::PatCommon
Functions
- check::pats::build_subst
- check::pats::mat::build_subst
- check::pats::mat::match_copat
- check::pats::mat::match_copats
- check::pats::mat::match_pat
- check::pats::mat::matched
- check::pats::match_copats
- check::rules::check
- check::rules::check_decls
- check::rules::clause::bind_as_and_tele
- check::rules::clause::clause
- check::rules::clause::clause_impl
- check::rules::clause::eqs::classify_eqs
- check::rules::clause::lhs::check_lhs
- check::rules::clause::lhs::final_check
- check::rules::clause::lhs::user_variable_names
- check::rules::clause::split::split_con
- check::rules::clause::split::split_tele
- check::rules::clause::state::insert_implicit_pats
- check::rules::clause::state::progress_lhs_state
- check::rules::data::check_cons
- check::rules::data::check_data
- check::rules::data::check_tele
- check::rules::decls::check_decls
- check::rules::infer
- check::rules::simplify
- check::rules::term::check
- check::rules::term::check_fallback
- check::rules::term::check_impl
- check::rules::term::infer::infer
- check::rules::term::infer::infer_head
- check::rules::term::infer::infer_head_impl
- check::rules::term::infer::infer_impl
- check::rules::term::infer::type_of_decl
- check::rules::term::meta::solve_meta
- check::rules::term::unify::check_solution
- check::rules::term::unify::compare_closure
- check::rules::term::unify::subtype
- check::rules::term::unify::subtype_impl
- check::rules::term::unify::unify_meta_with
- check::rules::term::unify::unify_val
- check::rules::term::view::expect_data
- check::rules::term::view::is_eta_var
- check::rules::term::view::is_eta_var_ref
- check::rules::term::whnf::elims_to_terms
- check::rules::term::whnf::simplify
- check::rules::term::whnf::unfold_func
- syntax::abs::desugar::decls::desugar_clause
- syntax::abs::desugar::decls::desugar_decl
- syntax::abs::desugar::decls::desugar_decls
- syntax::abs::desugar::decls::desugar_params
- syntax::abs::desugar::decls::desugar_pattern
- syntax::abs::desugar::decls::desugar_patterns
- syntax::abs::desugar::decls::desugar_telescope
- syntax::abs::desugar::decls::ops_range
- syntax::abs::desugar::desugar_main
- syntax::abs::desugar::exprs::desugar_expr
- syntax::core::pretty::pretty_application
- syntax::core::subst::apply::def_app
- syntax::core::subst::def_app
- syntax::surf::parse::app_expr
- syntax::surf::parse::applied
- syntax::surf::parse::clause
- syntax::surf::parse::clause_body
- syntax::surf::parse::codata
- syntax::surf::parse::codata_body
- syntax::surf::parse::cons_pat
- syntax::surf::parse::constructor
- syntax::surf::parse::constructors
- syntax::surf::parse::copattern
- syntax::surf::parse::data
- syntax::surf::parse::data_body
- syntax::surf::parse::decl
- syntax::surf::parse::decls
- syntax::surf::parse::definition
- syntax::surf::parse::dollar_expr
- syntax::surf::parse::dot_projection
- syntax::surf::parse::expr
- syntax::surf::parse::ident
- syntax::surf::parse::inacc_pat
- syntax::surf::parse::meta
- syntax::surf::parse::multi_param
- syntax::surf::parse::next_ident
- syntax::surf::parse::one_param
- syntax::surf::parse::param
- syntax::surf::parse::parse_ident
- syntax::surf::parse::parse_str
- syntax::surf::parse::parse_str_expr
- syntax::surf::parse::pattern
- syntax::surf::parse::pi_expr
- syntax::surf::parse::pi_expr_internal
- syntax::surf::parse::primary_expr
- syntax::surf::parse::projection
- syntax::surf::parse::projections
- syntax::surf::parse_expr_err_printed
- syntax::surf::parse_str
- syntax::surf::parse_str_err_printed
- syntax::surf::parse_str_expr
Typedefs
- check::monad::Sigma
- check::monad::TCM
- check::monad::TCMS
- check::monad::TermTCM
- check::monad::ValTCM
- check::monad::state::Sigma
- check::pats::CoreCopat
- check::pats::CorePat
- check::pats::RedM
- check::pats::core::CoreCopat
- check::pats::core::CorePat
- check::rules::clause::eqs::PatVars
- check::rules::term::infer::InferTCM
- syntax::abs::AbsCopat
- syntax::abs::AbsPat
- syntax::abs::AbsTele
- syntax::abs::Bind
- syntax::abs::ast::AbsCopat
- syntax::abs::ast::AbsPat
- syntax::abs::ast::AbsTele
- syntax::abs::ast::Bind
- syntax::abs::desugar::DesugarM
- syntax::abs::desugar::decls::DeclM
- syntax::abs::desugar::monad::DesugarM
- syntax::core::Bind
- syntax::core::Ctx
- syntax::core::Let
- syntax::core::LetList
- syntax::core::Tele
- syntax::core::TeleS
- syntax::core::ast::Bind
- syntax::core::ast::Let
- syntax::core::subst::Subst
- syntax::surf::ExprCons
- syntax::surf::ExprCopat
- syntax::surf::ExprPat
- syntax::surf::ExprProj
- syntax::surf::ast::ExprCons
- syntax::surf::ast::ExprCopat
- syntax::surf::ast::ExprPat
- syntax::surf::ast::ExprProj
- syntax::surf::parse::Tik
- syntax::surf::parse::Tok