package lambdapi
Proof assistant for the λΠ-calculus modulo rewriting
Install
Dune Dependency
Authors
Maintainers
Sources
lambdapi-2.5.1.tbz
sha256=2c251021b6fac40c05282ca183902da5b1008e69d9179d7a9543905c2c21a28a
sha512=69535f92766e6fedc2675fc214f0fb699bde2a06aa91d338c93c99756235a293cf16776f6328973dda07cf2ad402e58fe3104a08f1a896990c1778b42f7f9fcf
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)"
>