Reid Barton

I was imagining a series of options like `--with-host-compiler`, `--with-host-PROGRAM` to specify the compiler and program configuration to use for building Setup.hs. (And possibly in the future for building modules...

Apparently the Haskell-iPhone people are working around this by patching packages to use `build-type: Simple`. See the thread http://www.haskell.org/pipermail/iphone/2012-December/000180.html and some of the patches at https://github.com/kaoskorobase/ghc-ios-cabal-scripts/tree/master/patches, like lifted-base and syb.

I think I am encountering other issues with `prove_goal_async`, so I will hold off for a bit. Should `prove_goal_async` fail when the goal is not a Prop? Edit: by which...

Just guessing, but maybe there is a bad interaction with something like `parameter`s? As far as I know those can only appear inside a `section`.

Looking at the change 4946f5529085a38332110905fa61739e86b504f8 which introduced this restriction, and particularly the doc and test modifications, it looks like this change happened at a time when `constant` was used differently...

The crash is in `is_subobject_field` of `src/frontends/lean/structure_cmd.cpp`. Lean apparently thinks `S` is a structure which extends `foo` and then gets confused.

By the way, Lean won't let you name a structure field with something starting with an underscore, but using `inductive` as above bypasses this check.

@cipher1024, by "it", do you mean the change in default behavior, or using the `--old` flag? I'm expecting that someone generating `.olean` files from a non-Lean source also has some...

As you can probably guess from the error message, the expression `∀ h ∈ H, g * h * g⁻¹ ∈ H` is elaborated as `∀ h (H : h...

Without having examined all the examples for `combine` closely, I think it has a single clear purpose, though the documentation doesn't really state it. That purpose is: If `path1` names...