• OCaml logo OCaml logo
  • Learn
  • Packages
  • Community
  • Blog
  • Playground
  • Learn
  • Packages
  • Community
  • Blog
  • Playground
  • Get started
  • lambdapi
  • Documentation
  • lambdapi.tool lib
  • Tool .Sr Module
package lambdapi
  • lambdapi.common
    • Common
      • Console
        • State
      • Debug
        • D
      • Error
      • Escape
      • Library
        • LibMap
      • Logger
      • Path
        • Map
        • Path
        • Set
      • Pos
  • lambdapi.core
    • Core
      • Builtin
      • Ctxt
      • Env
      • Eval
      • Infer
      • Inverse
      • LibMeta
      • LibTerm
      • Print
      • Sig_state
      • Sign
      • Term
        • Meta
        • MetaMap
        • MetaSet
        • Raw
        • Sym
        • SymMap
        • SymSet
        • Var
        • VarMap
        • VarSet
      • Tree
        • CM
        • CP
          • PSet
      • Tree_type
        • TC
        • TCMap
      • Unif
      • Unif_rule
      • Version
  • lambdapi.export
    • Export
      • Dk
      • Hrs
      • Xtc
  • lambdapi.handle
    • Handle
      • Command
      • Compile
        • PureUpToSign
      • Inductive
      • Proof
        • Goal
      • Query
      • Rewrite
      • Tactic
      • Why3_tactic
  • lambdapi.lplib
    • Lplib
      • Array
      • Base
        • Int
      • Color
      • Extra
        • IntMap
        • IntSet
        • StrMap
        • StrSet
      • Filename
      • List
      • Option
      • Range
      • RangeMap
        • Make
          • 1-R
          • Range
      • RangeMap_intf
        • S
          • Range
      • Range_intf
        • S
      • String
  • lambdapi.lsp
    • Lsp
      • Lp_doc
      • Lp_lsp
      • Lsp_base
      • Lsp_io
  • lambdapi.parsing
    • Parsing
      • DkBasic
        • WS
      • DkLexer
      • DkParser
      • DkRule
      • DkTokens
      • LpLexer
      • LpParser
      • Package
      • Parser
        • Dk
        • Lp
        • PARSER
      • Pratt
        • Pratt
      • Pretty
      • Scope
      • Syntax
        • P
  • lambdapi.pure
    • Pure
      • Command
      • ProofTree
      • Tactic
  • lambdapi.tool
    • Tool
      • External
      • Lcr
      • Sr
      • Tree_graphviz
Legend:
Library
Module
Module type
Parameter
Class
Class type
val check_rule : Parsing.Scope.pre_rule Common.Pos.loc -> Core.Term.rule

check_rule r checks whether the pre-rule r is well-typed in signature state ss and then construct the corresponding rule. Note that Fatal is raised in case of error.

Footer

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS

About Us

  • Industrial Users
  • Academic Users
  • Why OCaml

Resources

  • Get Started
  • Language Manual
  • Standard Library API
  • Books
  • Releases

Community

  • Blog
  • Jobs

Policies

  • Carbon Footprint
  • Governance
  • Privacy
  • Code of Conduct