package rocq-runtime
The Rocq Prover -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
doc/src/cc_plugin/g_congruence.ml.html
Source file g_congruence.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 60 61 62# 11 "plugins/cc/g_congruence.mlg" open Ltac_plugin open Cctac open Stdarg let _ = Mltop.add_known_module "rocq-runtime.plugins.cc" let () = Tacentries.tactic_extend "rocq-runtime.plugins.cc" "cc" ~level:0 [(Tacentries.TyML (Tacentries.TyIdent ("congruence", Tacentries.TyArg ( Extend.TUopt ( Extend.TUentry (Genarg.get_arg_tag wit_natural)), Tacentries.TyNil)), (fun n ist -> # 25 "plugins/cc/g_congruence.mlg" congruence_tac n [] ))); (Tacentries.TyML (Tacentries.TyIdent ("congruence", Tacentries.TyArg ( Extend.TUopt ( Extend.TUentry (Genarg.get_arg_tag wit_natural)), Tacentries.TyIdent ("with", Tacentries.TyArg ( Extend.TUlist1 ( Extend.TUentry (Genarg.get_arg_tag wit_constr)), Tacentries.TyNil)))), (fun n l ist -> # 27 "plugins/cc/g_congruence.mlg" congruence_tac n l ))); (Tacentries.TyML (Tacentries.TyIdent ("simple", Tacentries.TyIdent ("congruence", Tacentries.TyArg ( Extend.TUopt ( Extend.TUentry (Genarg.get_arg_tag wit_natural)), Tacentries.TyNil))), (fun n ist -> # 29 "plugins/cc/g_congruence.mlg" simple_congruence_tac n [] ))); (Tacentries.TyML (Tacentries.TyIdent ("simple", Tacentries.TyIdent ("congruence", Tacentries.TyArg ( Extend.TUopt ( Extend.TUentry (Genarg.get_arg_tag wit_natural)), Tacentries.TyIdent ("with", Tacentries.TyArg ( Extend.TUlist1 ( Extend.TUentry (Genarg.get_arg_tag wit_constr)), Tacentries.TyNil))))), (fun n l ist -> # 31 "plugins/cc/g_congruence.mlg" simple_congruence_tac n l )))] let () = Tacentries.tactic_extend "rocq-runtime.plugins.cc" "f_equal" ~level:0 [(Tacentries.TyML (Tacentries.TyIdent ("f_equal", Tacentries.TyNil), (fun ist -> # 35 "plugins/cc/g_congruence.mlg" f_equal )))]