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

1160 commits

Author SHA1 Message Date
Leonardo de Moura
72aeab24eb chore: adjust new frontend 2020-05-12 15:07:06 -07:00
Leonardo de Moura
50990b99d6 chore: remove unnecessary annotations 2020-05-12 15:02:03 -07:00
Leonardo de Moura
ebfa362507 chore: fix HasOfNat 2020-05-12 15:02:03 -07:00
Leonardo de Moura
33a10130cf chore: fix stdlib 2020-05-12 15:02:03 -07:00
Sebastian Ullrich
f3976fc53a chore: parenthesizer: address some comments 2020-05-05 14:43:15 +02:00
Sebastian Ullrich
386c706f3e feat: basic parenthesizer 2020-05-04 14:28:36 -07:00
Sebastian Ullrich
822897e218 feat: lift MonadTracerAdapters 2020-05-04 14:28:36 -07:00
Sebastian Ullrich
942ed3a6a8 chore: set precedence of universe placeholder 2020-05-04 14:28:36 -07:00
Sebastian Ullrich
6a10e1254e fix: blockImplicitLambda: ignore parentheses 2020-05-04 14:28:36 -07:00
Sebastian Ullrich
11c3ada877 feat: add [parenthesizer] attribute 2020-05-04 14:28:36 -07:00
Sebastian Ullrich
28350f46d8 feat: prevent Windows error message boxes in all Lean programs 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
596a3af1a0 feat: check if "has already been declared" at the beginning 2020-04-09 15:29:10 -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
9a38aca8ec feat: add evalFailIfSuccess 2020-04-09 11:02:15 -07:00
Leonardo de Moura
539bb4a282 feat: add failIfSuccess tactic parser 2020-04-09 10:55:03 -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
fd61812b6e fix: wrong instance order for several instances 2020-04-08 16:55:48 -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
705530b62b fix: remove DecidableEq for Float 
We cannot implement `DecidableEq Float` using C equality for
`double`. Reason: the C implementation is not even reflexive.
If we need `DecidableEq Float`, we will need to provide our own
implementation (i.e., a wrapper around the one provided by the
hardware). In this commit, we implement `HasBeq Float` instead.

cc @dselsam
 2020-04-06 14:10:18 -07:00
Sebastian Ullrich
f66039f7f0 feat: generalize Array function universes 2020-04-06 13:48:09 -07:00
Leonardo de Moura
746615d81d chore: remove ⇒ as alternative for => 2020-04-06 13:45:22 -07:00
Leonardo de Moura
485034bbba fix: bug at ir.cpp 2020-04-03 17:39:28 -07:00
Leonardo de Moura
c236a179f2 feat: enable externs 2020-04-03 17:19:48 -07:00
Leonardo de Moura
0e2ebd36ff feat: make sure Float is in WHNF 2020-04-03 17:07:29 -07:00
Leonardo de Moura
b5f258773b feat: add Float 2020-04-03 16:49:32 -07:00
Leonardo de Moura
b0a02ef0bb feat: emit float runtime primitives 2020-04-03 16:02:35 -07:00
Leonardo de Moura
71397aad36 feat: runtime primitives 2020-04-03 15:55:39 -07:00
Leonardo de Moura
52cffcb67f feat: add Float.lean 2020-04-03 15:40:38 -07:00
Leonardo de Moura
af8bc28be0 fix: typo at IR.Expr.alphaEqv 2020-03-31 10:04:59 -07:00
Leonardo de Moura
0cbd09f967 chore: make sure generalizeTelescope signature is similar to other telescope methods 2020-03-30 11:43:41 -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
Leonardo de Moura
3c699eb915 feat: add mkAppOptM 2020-03-27 11:14:38 -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
Sebastian Ullrich
f39ea47376 chore: brackted ~> bracketed 2020-03-27 10:42:36 +01:00
Sebastian Ullrich
a79a2888d0 refactor: simplify delabLamAux 2020-03-27 10:42:36 +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
34ec66edb2 chore: re-enable {} and [] annotations at fun 2020-03-26 14:15:07 -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
e682c1c88f fix: make sure @ disable new syntax and macros too 
cc @Kha
 2020-03-26 12:14:55 -07:00
Leonardo de Moura
0c5a08a16e chore: make sure Delaborator.lean still compiles 
@Kha I removed `{}` `[]` from `funBinder`.
Please make sure `Delaborator.lean` still does what you want.
 2020-03-26 10:40:16 -07:00
Leonardo de Moura
19be2a5ade chore: remove {} and [] from funBinder 2020-03-26 10:40:16 -07:00