package lambdapi
Proof assistant for the λΠ-calculus modulo rewriting
Install
Dune Dependency
Authors
Maintainers
Sources
lambdapi-2.5.0.tbz
sha256=9bc8ae3694dd51bd5742e7aba760bd2878c4b0e5ef9b3d4a7b06f3cd303b611d
sha512=c812c3129b3d85b0c4d7e741d11137dbb4fe2a0aaba3a5968409080b742924ecb506280c19ad83ef6bc910346db96d87780313fa7683c29345edae16ae79c704
doc/src/lambdapi.lplib/base.ml.html
Source file base.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63
(** Standard library extension (mostly). *) (** Type of pretty-printing functions. *) type 'a pp = Format.formatter -> 'a -> unit (** Short name for a standard formatter. *) type 'a outfmt = ('a, Format.formatter, unit) format (** Short name for a standard formatter with continuation. *) type ('a, 'b) koutfmt = ('a, Format.formatter, unit, unit, unit, 'b) format6 let out = Format.fprintf let (++) (p1: 'a pp) (p2: 'b pp) : ('a * 'b) pp = fun ppf (arg1, arg2) -> out ppf "%a%a" p1 arg1 p2 arg2 let (|+) p1 p2 : 'a pp = fun ppf arg -> (p1 ++ p2) ppf ((), arg) let (+|) p1 p2 : 'a pp = fun ppf arg -> (p1 ++ p2) ppf (arg, ()) let int : int pp = Format.pp_print_int let string : string pp = Format.pp_print_string let float : float pp = fun ppf -> out ppf "%f" let unit : unit outfmt -> unit pp = fun fmt ppf () -> out ppf fmt let sep : string -> unit pp = fun s ff () -> string ff s let pp_if : bool -> 'a pp -> 'a pp = fun b pp ppf arg -> if b then out ppf "%a" pp arg let prefix : string -> 'a pp -> 'a pp = fun s pp ppf x -> out ppf "%s%a" s pp x let suffix : 'a pp -> string -> 'a pp = fun pp s ppf x -> out ppf "%a%s" pp x s (** Type of comparison functions. *) type 'a cmp = 'a -> 'a -> int (** Comparison function through a map. *) let cmp_map : 'b cmp -> ('a -> 'b) -> 'a cmp = fun cmpb f a1 a2 -> cmpb (f a1) (f a2) (** Tag comparison function. *) let cmp_tag : 'a cmp = fun t t' -> cmp_map Stdlib.compare (fun t -> Obj.tag (Obj.repr t)) t t' (** Lexicographic comparison. *) let lex : 'a cmp -> 'b cmp -> ('a * 'b) cmp = fun cmpa cmpb (a1,b1) (a2,b2) -> match cmpa a1 a2 with | 0 -> cmpb b1 b2 | n -> n let lex3 : 'a cmp -> 'b cmp -> 'c cmp -> ('a * 'b * 'c) cmp = fun cmpa cmpb cmpc (a1,b1,c1) (a2,b2,c2) -> lex cmpa (lex cmpb cmpc) (a1,(b1,c1)) (a2,(b2,c2)) (** Type of equality functions. *) type 'a eq = 'a -> 'a -> bool let eq_of_cmp : 'a cmp -> 'a eq = fun cmp x y -> cmp x y = 0 module Int = struct type t = int let compare = ( - ) end
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>