max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
19927 commits 1 branch 0 tags 5.3 GiB
Commit graph

4442 commits

Author SHA1 Message Date
Leonardo de Moura
a01552d361 chore: fix some tests 
Two of them are still broken due to a bug in the new elaborator.
 2020-05-21 09:50:20 -07:00
Leonardo de Moura
3ea9edbd13 chore: test for simulating old { Prod . ... } syntax 2020-05-20 16:06:57 -07:00
Leonardo de Moura
22ae065d16 feat: add { ... : <expected-type> } syntax 
It replaces the `{ <struct-name> . ... }` syntax.
 2020-05-20 15:24:27 -07:00
Leonardo de Moura
bd58048449 chore: { <source> with ... } syntax 2020-05-20 15:08:43 -07:00
Sebastian Ullrich
3d891be49e feat: delaborator: do not set whitespace information 2020-05-20 11:54:53 -07:00
Sebastian Ullrich
10253e89ea chore: move bin/ and .oleans into build directory 2020-05-14 14:47:54 +02:00
Sebastian Ullrich
053d4bab1c chore: factor out and unify common test behavior; retrieve lean from PATH 
`./test_single.sh foo.lean yes` is now `./test_single.sh -i foo.lean`
 2020-05-14 14:38:52 +02:00
Sebastian Ullrich
2325f5d358 chore: ignore more test output files 2020-05-14 14:38:52 +02:00
Sebastian Ullrich
bc40796729 chore: remove fail/ tests 
Checking for *any* failure is never a good idea. Use `$f.expected.ret` instead.
 2020-05-14 14:38:52 +02:00
Leonardo de Moura
ebc0663b3f chore: fix tests 2020-05-12 15:02:03 -07:00
Sebastian Ullrich
386c706f3e feat: basic parenthesizer 2020-05-04 14:28:36 -07:00
Sebastian Ullrich
e7920bcdb5 chore: remove test special case 2020-05-04 11:11:11 +02:00
Sebastian Ullrich
8f67db0101 refactor: never implicitly ignore monadic results 
Also change `do e; f` to desugar to `e *> f` so that it is affected as well
 2020-04-23 11:09:59 -07:00
Marc Huisinga
aa4fc12dff feat: translate and refactor Gabriel Ebner's JSON parser 
implement the JSON parser from https://github.com/gebner/lean4/tree/server by @gebner using new Lean 4 syntax and fix some minor bugs.
 2020-04-15 11:29:18 -07:00
Leonardo de Moura
7322345768 fix: private names 
@Kha I tried to fix a few issues with private names. The new test
tries to cover them. If you have more, please create an issue.

1- Scoping. A private declaration should shadow one in a previous scope.
2- We should not be able to define the same `private` in the same
module more than once.
   ```
   private def x := 10
   private def x := "hello" -- should produce error here
   ```
3- Dot-notation should work with private declarations in the module
where they were defined.
4- The following should work
   ```
   namespace N
   private def x := 10
   end N
   #check N.x
   ```
5- The following should **not** work
   ```
   def y := 10
   private def y := "hello" -- produce error

   private def z := 10
   def z := "hello" -- produce error
   ```
   BTW, I am happy to change this behavior. I just mimicked C's
   behavior for `static`.

It is not clear whether the following should work or not.
```
    namespace N
      private def b := 10
    end N
    open N
    #check b
```
 2020-04-09 16:28:21 -07:00
Leonardo de Moura
360cebf680 fix: induction tactic must check expected major premise type 
`whnfUntil` now returns `Option Expr`.
 2020-04-09 11:18:02 -07:00
Leonardo de Moura
9a5bed0f94 fix: missing ! at whnfUntil 2020-04-09 10:49:20 -07:00
Leonardo de Moura
7a5fcfae8b feat: add [recursor] attribute to Iff.elim 2020-04-09 10:45:27 -07:00
Leonardo de Moura
40336131bb feat: do not switch to term mode in the RHS of induction and cases tactics 2020-04-08 17:45:06 -07:00
Daniel Selsam
7c1c0dc01e test: example that requires the instance arg reordering 2020-04-08 16:56:14 -07:00
Leonardo de Moura
e22af8d1ef feat: add FloatArray 
cc @dselsam
 2020-04-07 18:05:54 -07:00
Leonardo de Moura
b8ea55c989 feat: expose some transcendental functions from the C library 
cc @dselsam
 2020-04-06 15:22:25 -07:00
Leonardo de Moura
8e84a8c9ec feat: Float from big numbers 2020-04-06 14:05:17 -07:00
Leonardo de Moura
746615d81d chore: remove ⇒ as alternative for => 2020-04-06 13:45:22 -07:00
Leonardo de Moura
22fc56f5c8 chore: fix test 2020-03-31 10:10:57 -07:00
Leonardo de Moura
af8bc28be0 fix: typo at IR.Expr.alphaEqv 2020-03-31 10:04:59 -07:00
Daniel Selsam
722ea2b694 failing test for suspicious behavior 2020-03-31 10:03:22 -07:00
Sebastian Ullrich
b6fc9428f1 fix: support Windows newlines and '\r' escape 2020-03-27 13:21:21 -07:00
Leonardo de Moura
0595e8a78a feat: add tryPureCoe 
@Kha It seems to work reasonably well. It didn't break any test.
 2020-03-27 11:20:43 -07:00
Sebastian Ullrich
fcdbdeecaf feat: delaborator: use implicit lambdas where possible 
/cc @leodemoura it's not bullet-proof (unless `pp.explicit` is set), but let's
see if it is good enough in practice
 2020-03-27 14:55:46 +01:00
Sebastian Ullrich
db93638a96 feat: delab forallE 2020-03-27 11:59:58 +01:00
Leonardo de Moura
02acdee9ce feat: disable implicit lambda insertion for fun containing {} or [] 
cc @Kha
 2020-03-26 14:32:12 -07:00
Leonardo de Moura
b4b5f2736f feat: elaborate [] and {} binder annotations in lambda abstractions 
We can simulate Lean3 behavior.
 2020-03-26 14:20:39 -07:00
Leonardo de Moura
07ffa535fe refactor: decide whether to insert implicit lambdas AFTER macro expansion 
cc @Kha
 2020-03-26 13:53:15 -07:00
Leonardo de Moura
2b3bdbe0cf test: implicit lambdas + notation 2020-03-26 12:31:04 -07:00
Leonardo de Moura
e682c1c88f fix: make sure @ disable new syntax and macros too 
cc @Kha
 2020-03-26 12:14:55 -07:00
Leonardo de Moura
6625656940 refactor: remove support for fun {a : A} => ... 
The semantics was weird. It seems Agda is also having problems with
it. Here is an example that demonstrates how weird the semantics is:

```lean
check (fun {β α} (a : α) (b : β) => (b, a) : {α : Type} → {β : Type} → (a : α) → (b : β) → β × α)

-- Same example using `def`
def f : {α : Type} → {β : Type} → α → β → β × α :=
fun {β : Type} {α : Type} (a : α) (b : β) => (b, a)
```

Both commands were being accepted before this commit. Note that it
flips `β` and `α`.

Here is an example that did not work before this commit and would
confuse users.

```lean
check
  let id := fun {α} (a : α) => a;
  id [id 1]
```

users would have to write

```lean
check
  let id {α} (a : α) := a;
  id [id 1]
```

@Kha The Delaborator.lean test broke and I "fixed" by removing the
`{}` from it, and copying `produced` over `expected`. Please make sure
it still makes sense.
 2020-03-26 10:40:16 -07:00
Leonardo de Moura
d79cfa38e3 test: generalizeTelescope tests 2020-03-25 16:00:55 -07:00
Sebastian Ullrich
6ffe310c48 feat: delab coercions 2020-03-24 17:27:10 +01:00
Sebastian Ullrich
fdc03c9d74 feat: delab projections 2020-03-24 17:27:02 +01:00
Leonardo de Moura
2ca347fcd6 chore: fix test 2020-03-23 15:47:51 -07:00
Leonardo de Moura
dc80b76106 feat: add IO.FS.lines 2020-03-23 14:53:27 -07:00
Leonardo de Moura
94f016a3e8 fix: readLine and test 2020-03-23 14:06:17 -07:00
Leonardo de Moura
db914052ce fix: IO.getLine 2020-03-23 12:26:09 -07:00
Leonardo de Moura
4296e1d83e feat: add tests for Closure.lean 2020-03-20 18:32:04 -07:00
Sebastian Ullrich
7f09973d43 feat: basic delaborator 2020-03-19 17:17:34 -07:00
Sebastian Ullrich
ed14375dad feat: sort and deduplicate "expected" tokens in parser error messages 2020-03-19 17:17:08 -07:00
Leonardo de Moura
eaaaaabc60 feat: allow Lean.Parser.Term.id to be used in binders 
cc @Kha
 2020-03-18 20:54:08 -07:00
Leonardo de Moura
2954f6ad3e feat: add MetaHasEval instance for TermElabM 
cc @Kha
 2020-03-18 20:09:14 -07:00
Leonardo de Moura
5d35b2c419 test: decide! tests 2020-03-18 16:48:28 -07:00