max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/module): has_sorry: check examples

Browse source
This commit is contained in:
Gabriel Ebner 2017-02-24 14:46:47 +01:00
parent c6ccda0f98
commit 9bcfc06bd0
7 changed files with 13 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/module.cpp
View file

@ -444,8 +444,10 @@ struct add_decl_sorry_check : public task<unit> {
return optional<name>();
if (!is_internal_name(n))
return optional<name>(n);
if (!n.is_string() || n.is_atomic())
if (!n.is_string())
return optional<name>();
if (strcmp(n.get_string(), "_example") == 0)
return optional<name>(n);
if (strcmp(n.get_string(), "_main") == 0)
return should_report_sorry(n.get_prefix());
if (strncmp(n.get_string(), "_match", 6) == 0) {

3
tests/lean/1369.lean.expected.out
View file

@ -1,4 +1,7 @@
1369.lean:15:8: warning: declaration '_example' uses sorry
17 ≤ 555555
⊢ 17 ≤ 555555
1369.lean:21:8: warning: declaration '_example' uses sorry
?m_1 ≤ 555555
⊢ ?m_1 ≤ 555555
1369.lean:33:8: warning: declaration '_example' uses sorry

1
tests/lean/anc1.lean.expected.out
View file

@ -1,5 +1,6 @@
(1, 2) : ℕ × ℕ
and.intro trivial trivial : true ∧ true
anc1.lean:5:8: warning: declaration '_example' uses sorry
{fst := 1, snd := sorry} : Σ' (x : ℕ), x > 0
show true, from true.intro : true
Exists.intro 1 (id_locked (1 ≠ 0) (λ (a : 1 = 0), nat.no_confusion a)) : ∃ (x : ℕ), 1 ≠ 0

1
tests/lean/bad_error2.lean.expected.out
View file

@ -7,3 +7,4 @@ _match : (∃ (k_1 : ℕ), k + n + k_1 = k + m) → n ≤ m,
w : ℕ,
hw : (λ (k_1 : ℕ), k + n + k_1 = k + m) w
⊢ n + w = m
bad_error2.lean:3:8: warning: declaration '_example' uses sorry

1
tests/lean/error_pos.lean.expected.out
View file

@ -1,5 +1,6 @@
error_pos.lean:1:39: error: type expected at
B
error_pos.lean:1:8: warning: declaration '_example' uses sorry
error_pos.lean:4:43: error: type expected at
B
error_pos.lean:9:39: error: type expected at

1
tests/lean/quot_bug.lean.expected.out
View file

@ -1 +1,2 @@
λ (x : A), f x
quot_bug.lean:8:8: warning: declaration '_example' uses sorry

3
tests/lean/vm_sorry.lean.expected.out
View file

@ -3,3 +3,6 @@ vm_sorry.lean:1:4: warning: declaration 'half_baked' uses sorry
vm_sorry.lean:6:0: error: half_baked._main._val_1: trying to evaluate sorry
vm_sorry.lean:12:0: error: undefined
(some nat)
vm_sorry.lean:18:8: warning: declaration '_example' uses sorry
vm_sorry.lean:19:8: warning: declaration '_example' uses sorry
vm_sorry.lean:20:8: warning: declaration '_example' uses sorry