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