max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Init/Lean/Meta
History
Leonardo de Moura 3de7d6d5c3 fix: remove mvarTypeNotWellFormedInSmallerLCtx 
We use `check` recursively instead of `isWellFormed`.

@kha This was the last bug for the repro
```
```
This example works now, but I am sure there are many other bugs.
2020-01-07 16:56:10 -08:00
..
Tactic feat: split synthetic into synthetic and syntheticOpaque 2019-12-16 17:06:45 -08:00
AbstractMVars.lean chore: naming convention 2019-12-15 18:28:00 -08:00
AppBuilder.lean feat: split synthetic into synthetic and syntheticOpaque 2019-12-16 17:06:45 -08:00
Basic.lean feat: add mkForallUsedOnly 2020-01-05 11:53:39 -08:00
Check.lean chore: naming convention 2019-12-15 07:48:42 -08:00
DiscrTree.lean feat: split synthetic into synthetic and syntheticOpaque 2019-12-16 17:06:45 -08:00
DiscrTreeTypes.lean feat: add synthInstance cache 2019-12-01 18:32:48 -08:00
Exception.lean chore: combine MessageData.context + MessageData.withOptions into MessageData.context 2019-12-22 09:15:04 -08:00
ExprDefEq.lean fix: remove mvarTypeNotWellFormedInSmallerLCtx 2020-01-07 16:56:10 -08:00
FunInfo.lean chore: naming convention 2019-12-15 18:28:00 -08:00
InferType.lean fix: unregistered level metavariable 2019-12-19 09:58:05 -08:00
Instances.lean feat: applyAttributes 2020-01-05 16:22:46 -08:00
LevelDefEq.lean chore: add stuck trace message 2020-01-07 12:56:15 -08:00
Message.lean chore: combine MessageData.context + MessageData.withOptions into MessageData.context 2019-12-22 09:15:04 -08:00
Offset.lean chore: move Lean auxiliary datatypes to src/Init/Lean/Data 2019-12-04 17:00:13 -08:00
Reduce.lean feat: add reduce 2019-11-25 08:42:23 -08:00
SynthInstance.lean fix: typos in SynthInstance.lean 2020-01-03 10:29:01 -08:00
Tactic.lean feat: add intro and assumption 2019-12-05 10:57:48 -08:00
WHNF.lean chore: naming convention 2019-12-15 18:28:00 -08:00