package lambdapi

  1. Overview
  2. Docs
Proof assistant for the λΠ-calculus modulo rewriting

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (11)

Authors

  1. D
    Deducteam

Maintainers

  1. D
    dedukti-dev@inria.fr

Sources

lambdapi-2.5.0.tbz
sha256=9bc8ae3694dd51bd5742e7aba760bd2878c4b0e5ef9b3d4a7b06f3cd303b611d
sha512=c812c3129b3d85b0c4d7e741d11137dbb4fe2a0aaba3a5968409080b742924ecb506280c19ad83ef6bc910346db96d87780313fa7683c29345edae16ae79c704

doc/lambdapi.parsing/Parsing/LpLexer/index.html

Module Parsing.LpLexerSource

Sourceval __sedlex_table_22 : string
Sourceval __sedlex_table_26 : string
Sourceval __sedlex_table_49 : string
Sourceval __sedlex_table_20 : string
Sourceval __sedlex_table_1 : string
Sourceval __sedlex_table_2 : string
Sourceval __sedlex_table_3 : string
Sourceval __sedlex_table_4 : string
Sourceval __sedlex_table_5 : string
Sourceval __sedlex_table_6 : string
Sourceval __sedlex_table_7 : string
Sourceval __sedlex_table_8 : string
Sourceval __sedlex_table_9 : string
Sourceval __sedlex_table_10 : string
Sourceval __sedlex_table_11 : string
Sourceval __sedlex_table_12 : string
Sourceval __sedlex_table_13 : string
Sourceval __sedlex_table_14 : string
Sourceval __sedlex_table_15 : string
Sourceval __sedlex_table_17 : string
Sourceval __sedlex_table_18 : string
Sourceval __sedlex_table_19 : string
Sourceval __sedlex_table_21 : string
Sourceval __sedlex_table_24 : string
Sourceval __sedlex_table_25 : string
Sourceval __sedlex_table_27 : string
Sourceval __sedlex_table_28 : string
Sourceval __sedlex_table_30 : string
Sourceval __sedlex_table_31 : string
Sourceval __sedlex_table_32 : string
Sourceval __sedlex_table_33 : string
Sourceval __sedlex_table_35 : string
Sourceval __sedlex_table_36 : string
Sourceval __sedlex_table_37 : string
Sourceval __sedlex_table_38 : string
Sourceval __sedlex_table_39 : string
Sourceval __sedlex_table_40 : string
Sourceval __sedlex_table_42 : string
Sourceval __sedlex_table_43 : string
Sourceval __sedlex_table_44 : string
Sourceval __sedlex_table_45 : string
Sourceval __sedlex_table_46 : string
Sourceval __sedlex_table_47 : string
Sourceval __sedlex_table_48 : string
Sourceval __sedlex_table_50 : string
Sourceval __sedlex_table_51 : string
Sourceval __sedlex_table_52 : string
Sourceval __sedlex_table_53 : string
Sourceval __sedlex_table_54 : string
Sourceval __sedlex_table_55 : string
Sourceval __sedlex_table_56 : string
Sourceval __sedlex_table_57 : string
Sourceval __sedlex_table_58 : string
Sourceval __sedlex_table_60 : string
Sourceval __sedlex_table_62 : string
Sourceval __sedlex_table_63 : string
Sourceval __sedlex_table_64 : string
Sourceval __sedlex_table_65 : string
Sourceval __sedlex_table_66 : string
Sourceval __sedlex_table_67 : string
Sourceval __sedlex_table_68 : string
Sourceval __sedlex_table_34 : string
Sourceval __sedlex_table_59 : string
Sourceval __sedlex_table_16 : string
Sourceval __sedlex_table_41 : string
Sourceval __sedlex_table_23 : string
Sourceval __sedlex_table_29 : string
Sourceval __sedlex_table_61 : string
Sourceval __sedlex_partition_48 : int -> int
Sourceval __sedlex_partition_58 : int -> int
Sourceval __sedlex_partition_20 : int -> int
Sourceval __sedlex_partition_25 : int -> int
Sourceval __sedlex_partition_41 : int -> int
Sourceval __sedlex_partition_42 : int -> int
Sourceval __sedlex_partition_69 : int -> int
Sourceval __sedlex_partition_8 : int -> int
Sourceval __sedlex_partition_66 : int -> int
Sourceval __sedlex_partition_21 : int -> int
Sourceval __sedlex_partition_38 : int -> int
Sourceval __sedlex_partition_57 : int -> int
Sourceval __sedlex_partition_64 : int -> int
Sourceval __sedlex_partition_16 : int -> int
Sourceval __sedlex_partition_63 : int -> int
Sourceval __sedlex_partition_28 : int -> int
Sourceval __sedlex_partition_50 : int -> int
Sourceval __sedlex_partition_10 : int -> int
Sourceval __sedlex_partition_12 : int -> int
Sourceval __sedlex_partition_17 : int -> int
Sourceval __sedlex_partition_52 : int -> int
Sourceval __sedlex_partition_68 : int -> int
Sourceval __sedlex_partition_4 : int -> int
Sourceval __sedlex_partition_32 : int -> int
Sourceval __sedlex_partition_15 : int -> int
Sourceval __sedlex_partition_19 : int -> int
Sourceval __sedlex_partition_33 : int -> int
Sourceval __sedlex_partition_26 : int -> int
Sourceval __sedlex_partition_72 : int -> int
Sourceval __sedlex_partition_49 : int -> int
Sourceval __sedlex_partition_65 : int -> int
Sourceval __sedlex_partition_7 : int -> int
Sourceval __sedlex_partition_54 : int -> int
Sourceval __sedlex_partition_44 : int -> int
Sourceval __sedlex_partition_55 : int -> int
Sourceval __sedlex_partition_67 : int -> int
Sourceval __sedlex_partition_14 : int -> int
Sourceval __sedlex_partition_53 : int -> int
Sourceval __sedlex_partition_39 : int -> int
Sourceval __sedlex_partition_9 : int -> int
Sourceval __sedlex_partition_23 : int -> int
Sourceval __sedlex_partition_24 : int -> int
Sourceval __sedlex_partition_40 : int -> int
Sourceval __sedlex_partition_2 : int -> int
Sourceval __sedlex_partition_46 : int -> int
Sourceval __sedlex_partition_51 : int -> int
Sourceval __sedlex_partition_61 : int -> int
Sourceval __sedlex_partition_3 : int -> int
Sourceval __sedlex_partition_31 : int -> int
Sourceval __sedlex_partition_37 : int -> int
Sourceval __sedlex_partition_47 : int -> int
Sourceval __sedlex_partition_71 : int -> int
Sourceval __sedlex_partition_13 : int -> int
Sourceval __sedlex_partition_1 : int -> int
Sourceval __sedlex_partition_36 : int -> int
Sourceval __sedlex_partition_43 : int -> int
Sourceval __sedlex_partition_59 : int -> int
Sourceval __sedlex_partition_62 : int -> int
Sourceval __sedlex_partition_27 : int -> int
Sourceval __sedlex_partition_34 : int -> int
Sourceval __sedlex_partition_45 : int -> int
Sourceval __sedlex_partition_56 : int -> int
Sourceval __sedlex_partition_11 : int -> int
Sourceval __sedlex_partition_18 : int -> int
Sourceval __sedlex_partition_6 : int -> int
Sourceval __sedlex_partition_60 : int -> int
Sourceval __sedlex_partition_70 : int -> int
Sourceval __sedlex_partition_74 : int -> int
Sourceval __sedlex_partition_22 : int -> int
Sourceval __sedlex_partition_30 : int -> int
Sourceval __sedlex_partition_35 : int -> int
Sourceval __sedlex_partition_73 : int -> int
Sourceval __sedlex_partition_29 : int -> int
Sourceval __sedlex_partition_5 : int -> int

Lexer for Lambdapi syntax, using Sedlex, a Utf8 lexer generator.

Sourceval remove_first : Sedlexing.lexbuf -> string
Sourceval remove_last : Sedlexing.lexbuf -> string
Sourceval remove_ends : Sedlexing.lexbuf -> string
Sourceexception SyntaxError of Common.Pos.strloc
Sourceval syntax_error : (Lexing.position * Lexing.position) -> string -> 'a
Sourceval fail : Sedlexing.lexbuf -> string -> 'a
Sourceval invalid_character : Sedlexing.lexbuf -> 'a
Sourcetype token =
  1. | EOF
  2. | ABORT
  3. | ADMIT
  4. | ADMITTED
  5. | APPLY
  6. | AS
  7. | ASSERT of bool
  8. | ASSOCIATIVE
  9. | ASSUME
  10. | BEGIN
  11. | BUILTIN
  12. | COERCE_RULE
  13. | COMMUTATIVE
  14. | COMPUTE
  15. | CONSTANT
  16. | DEBUG
  17. | END
  18. | FAIL
  19. | FLAG
  20. | GENERALIZE
  21. | HAVE
  22. | IN
  23. | INDUCTION
  24. | INDUCTIVE
  25. | INFIX
  26. | INJECTIVE
  27. | LET
  28. | NOTATION
  29. | OPAQUE
  30. | OPEN
  31. | POSTFIX
  32. | PREFIX
  33. | PRINT
  34. | PRIVATE
  35. | PROOFTERM
  36. | PROTECTED
  37. | PROVER
  38. | PROVER_TIMEOUT
  39. | QUANTIFIER
  40. | REFINE
  41. | REFLEXIVITY
  42. | REMOVE
  43. | REQUIRE
  44. | REWRITE
  45. | RULE
  46. | SEARCH
  47. | SEQUENTIAL
  48. | SIMPLIFY
  49. | SOLVE
  50. | SYMBOL
  51. | SYMMETRY
  52. | TRY
  53. | TYPE_QUERY
  54. | TYPE_TERM
  55. | UNIF_RULE
  56. | VERBOSE
  57. | WHY3
  58. | WITH
  59. | DEBUG_FLAGS of bool * string
  60. | NAT of string
  61. | FLOAT of string
  62. | SIDE of Pratter.associativity
  63. | STRINGLIT of string
  64. | SWITCH of bool
  65. | ARROW
  66. | ASSIGN
  67. | BACKQUOTE
  68. | COMMA
  69. | COLON
  70. | DOT
  71. | EQUIV
  72. | HOOK_ARROW
  73. | LAMBDA
  74. | L_CU_BRACKET
  75. | L_PAREN
  76. | L_SQ_BRACKET
  77. | PI
  78. | R_CU_BRACKET
  79. | R_PAREN
  80. | R_SQ_BRACKET
  81. | SEMICOLON
  82. | TURNSTILE
  83. | UNDERSCORE
  84. | VBAR
  85. | UID of string
  86. | UID_EXPL of string
  87. | UID_META of int
  88. | UID_PATT of string
  89. | QID of Common.Path.t
  90. | QID_EXPL of Common.Path.t

Tokens.

Identifiers.

There are two kinds of identifiers: regular identifiers and escaped identifiers of the form "{|...|}".

Modulo those surrounding brackets, escaped identifiers allow to use as identifiers keywords or filenames that are not regular identifiers.

An escaped identifier denoting a filename or directory is unescaped before accessing to it. Hence, the module "{|a b|}" refers to the file "a b".

Identifiers need to be normalized so that an escaped identifier, once unescaped, is not regular. To this end, every identifier of the form "{|s|}" with s regular, is understood as "s" (function remove_useless_escape below).

Finally, identifiers must not be empty, so that we can use the empty string for the path of ghost signatures.

Sourceval is_regid : string -> bool
Sourceval escape : string -> string

escape s converts a string s into an escaped identifier if it is not regular. We do not check whether s contains "|}". FIXME?

Sourceval remove_useless_escape : string -> string

remove_useless_escape s replaces escaped regular identifiers by their unescape form.

Sourceval qid : bool -> string list -> Sedlexing.lexbuf -> token
Sourceval comment : (Sedlexing.lexbuf -> token) -> int -> Sedlexing.lexbuf -> token
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct