lean2/tests/lean/redundant_pattern.lean.expected.out at bccf716fd574a32f3d9295af9588dfbb63ae48d9 - michael/lean2 - Forgejo: Beyond coding. We forge.

michael/lean2

Leonardo de Moura 950f356d9a refactor(library/blast,frontends/lean): forward pattern index

2015-12-02 22:52:55 -08:00

4 lines

203 B

Text

Raw Blame History

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

 definition foo [forward] : ∀ (m n k : ℕ), P (f m) → P (g n) → P (f k) → P k ∧ R (g m) (f n) ∧ P (g m) ∧ P (f n) :=
 λ (m n k : ℕ), sorry
 (multi-)patterns:
 {P ?M_1, R (g ?M_2) (f ?M_3)}