package lambdapi
Proof assistant for the λΠ-calculus modulo rewriting
Install
Dune Dependency
Authors
Maintainers
Sources
lambdapi-2.6.0.tbz
sha256=d01e5f13db2eaba6e4fe330667149e0059d4886c651ff9d6b672db2dfc9765ed
sha512=33b68c972aca37985ed73c527076198e7d4961c7e27c89cdabfe4d1cff97cd41ccfb85ae9499eb98ad9a0aefd920bc55555df6393fc441ac2429e4d99cddafa8
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)"
>