Mentions légales du service

Skip to content
Snippets Groups Projects
Closed instantiate should be able to remove the general hypothesis
  • View options
  • instantiate should be able to remove the general hypothesis

  • View options
  • Closed Issue created by DAILLER Sylvain

    Add an optional argument so that on hypothesis:

    H : forall x. x = 0

    instantiate H 1 generate the following hypotheses (name change and remove hypothesis):

    H : 1 = 0

    instead of

    H : forall x. x = 0
    H_inst : 1 = 0

    Linked items ... 0

  • Activity

    • All activity
    • Comments only
    • History only
    • Newest first
    • Oldest first
    Loading Loading Loading Loading Loading Loading Loading Loading Loading Loading