diff options
| author | Hugo Herbelin | 2015-12-03 14:59:27 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-03 15:07:37 +0100 |
| commit | 281bed69ee7d4a7638d07f07f9d6722b897f29cc (patch) | |
| tree | 737464832cbc0a830371cb28c8002f0d34f8b140 /dev | |
| parent | 6316e8b380a9942cd587f250eb4a69668e52019e (diff) | |
Improving over printing of let-tuple (see #4447).
For instance, #4447 is now printed:
λ Ca Da : ℕAlg,
let (ℕ, ℕ0) := (Ca, Da) in
let (C, p) := ℕ in
let (c₀, cs) := p in
let (D, p0) := ℕ0 in
let (d₀, ds) := p0 in
{h : C → D & ((h c₀ = d₀) * (∀ c : C, h (cs c) = ds (h c)))%type}
: ℕAlg → ℕAlg → Type
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions
