package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

start_deriving f suchthat lemma starts a proof of suchthat (which can contain references to f) in the context extended by f:=?x. When the proof ends, f is defined as the value of ?x and lemma as the proof.

OCaml

Innovation. Community. Security.