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/option.ml.html
Source file option.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
open Base include Stdlib.Option type 'a t = 'a option let is_None : 'a t -> bool = fun o -> match o with None -> true | Some _ -> false let get : 'a -> 'a option -> 'a = fun d o -> match o with None -> d | Some e -> e let map_default : ('a -> 'b) -> 'b -> 'a option -> 'b = fun f d o -> match o with None -> d | Some e -> f e let fold : ('a -> 'b -> 'a) -> 'a -> 'b option -> 'a = fun f a o -> match o with None -> a | Some b -> f a b let cmp : 'a cmp -> 'a option cmp = fun cmp_elt o o' -> match o, o' with | None, None -> 0 | None, Some _ -> -1 | Some _, None -> 1 | Some x, Some x' -> cmp_elt x x' let eq : 'a eq -> 'a option eq = fun eq_elt o1 o2 -> match o1, o2 with | None, None -> true | Some e1, Some e2 -> eq_elt e1 e2 | _ -> false let pp : 'a pp -> 'a option pp = fun elt ppf o -> match o with None -> () | Some e -> elt ppf e module Monad = struct let ( let* ) = Stdlib.Option.bind (** Monadic [let*] allows to replace {[ match e1 with | Some e2 -> Some (f e2) | None -> None ]} with {[ let* x = e1 in f x ]} *) let return x = Some x end module Applicative = struct let pure x = Some x let ( <*> ) : ('a -> 'b) option -> 'a option -> 'b option = fun o x -> match o with | Some f -> map f x | None -> None end
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>