Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Possible typo #1

Closed
wants to merge 24 commits into from
Closed

Possible typo #1

wants to merge 24 commits into from

Conversation

dselsam
Copy link

@dselsam dselsam commented Dec 1, 2015

No description provided.

leodemoura and others added 24 commits November 26, 2015 11:41
@leodemoura
feat(frontends/lean/decl_attributes): turn on [forward] if pattern …
40e9fe7 
…hints have been provided
@leodemoura
fix(library/blast/forward/pattern): missing case
d4bd6d5
@leodemoura
fix(frontends/lean/builtin_cmds): print patterns
6b7c52a
@leodemoura
fix(frontends/lean/builtin_cmds): private constants in the print command
5657050
@leodemoura
chore(library/blast/forward/forward_extension): rename procedure
c1c1db7
@leodemoura
feat(library/blast/forward/ematch): ematching skeleton
15a3e1f
@leodemoura
feat(library/blast/forward/pattern): save meta-variables
f2a4cd5
@leodemoura
feat(library/blast): add blast.ematch option, and ematching search pr…
2789d90 
…ocedure
@leodemoura
fix(src/library/blast/forward/ematch): use head_index at m_apps
1bde8f4
@leodemoura
fix(library/blast/forward/ematch): extract lemma using target express…
112e289 
…ion instead of pattern

Reason: pattern contains temporary universe meta-variables.
@leodemoura
fix(library/type_context): improve on_is_def_eq_failure
a63c706
@leodemoura
feat(library/blast/forward/ematch): use type class resolution to infe…
729e068 
…r missing arguments
@leodemoura
feat(library/idx_metavar): add has_idx_metavar
7ec15be
@leodemoura
feat(library/blast/forward/ematch): generate new instances
ad1eb32
@leodemoura
test(tests/lean/run): add basic ematching tests
06bc15f
@leodemoura
fix(library/blast/congruence_closure): bug in congruence closure proo…
1876d1e 
…f extraction
@leodemoura
feat(library/blast): add blast.backward option for disabling/enabling…
cb26c4f 
… backward chaining
@leodemoura
feat(library/blast/forward/ematch): add support for multi-patterns
388c43d
@leodemoura
fix(library/blast/options): typo
cdf2485
@leodemoura
chore(tests/lean/run/blast_ematch5): disable unnecessary options
f8562ae
@leodemoura
test(tests/lean/run): add new test
02c79b5
@leodemoura
test(tests/lean/run): add Daniel's example
1572325
@leodemoura
test(tests/lean/run): add more tests from algebra
76fa8c6
@dselsam
Possible typo
8d376b3
@leodemoura leodemoura closed this Dec 3, 2015
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@dselsam @leodemoura