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.core/coercion.ml.html
Source file coercion.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
open Common open Term let coerce : sym = let id = Pos.none "coerce" in Sign.add_symbol Ghost.sign Public Defin Eager false id None mk_Kind [] let apply a b t : term = add_args (mk_Symb coerce) [a; b; t] let _ = (* Add the rule [coerce $A $A $t ↪ $t] (but we don't have access to the parser here) *) let rule = let lhs = [ mk_Patt (Some 0, "A", [||]) ; mk_Patt (Some 0, "A", [||]) ; mk_Patt (Some 1, "t", [||]) ] in let vars = [|new_tevar "A"; new_tevar "t"|] in let rhs = _TEnv (_TE_Vari vars.(1)) [||] in let rhs = Bindlib.(bind_mvar vars rhs |> unbox) in let arity = 3 in let arities = [|0; 0|] in { lhs; rhs; arity; arities; vars; xvars_nb = 0; rule_pos = None } in Sign.add_rule Ghost.sign coerce rule
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>