-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathout
23 lines (23 loc) · 755 Bytes
/
out
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
/Users/matt/GitHub/lean-autograding/src/assignment.lean:9:0: warning: declaration 'another_exercise' uses sorry
/Users/matt/GitHub/lean-autograding/src/assignment.lean:11:6: error: definition 'yet_another_exercise' is noncomputable, it depends on 'duh'
/Users/matt/GitHub/lean-autograding/.test/test2.lean:3:0: warning: imported file '/Users/matt/GitHub/lean-autograding/src/assignment.lean' uses sorry
Problem 1
no axioms
---
Problem 2
[sorry]
no axioms
---
/Users/matt/GitHub/lean-autograding/.test/test2.lean:43:8: error: definition 'check_problem3' is noncomputable, it depends on 'yet_another_exercise'
Problem 3
duh
doh
dah
---
/Users/matt/GitHub/lean-autograding/.test/test2.lean:54:2: error: failed
state:
⊢ bool
Problem 4
[sorry]
no axioms
---