Fix indent
This commit is contained in:
parent
0d8ecdf816
commit
a1eeafaf38
|
@ -6,7 +6,3 @@
|
|||
< [(typeof Γ M (σ → σ_2))
|
||||
---
|
||||
> [(typeof Γ M (σ_2 → σ_2))
|
||||
261c261
|
||||
< M]
|
||||
---
|
||||
> M]
|
||||
|
|
|
@ -5,7 +5,7 @@
|
|||
48d47
|
||||
< (([cons @ τ] v) v)
|
||||
261,262c260
|
||||
< M]
|
||||
< M]
|
||||
< [#f #f]))
|
||||
---
|
||||
> M]))
|
||||
|
|
|
@ -6,7 +6,3 @@
|
|||
< [(typeof Γ M (σ → σ_2))
|
||||
---
|
||||
> [(typeof Γ M (σ_2 → σ))
|
||||
261c261
|
||||
< M]
|
||||
---
|
||||
> M]
|
||||
|
|
|
@ -6,7 +6,3 @@
|
|||
< (∀ a (a → ((list a) → (list a))))]
|
||||
---
|
||||
> (∀ a (a → ((list a) → a)))]
|
||||
261c261
|
||||
< M]
|
||||
---
|
||||
> M]
|
||||
|
|
|
@ -6,7 +6,3 @@
|
|||
< (in-hole E v_2)
|
||||
---
|
||||
> (in-hole E v_1)
|
||||
261c261
|
||||
< M]
|
||||
---
|
||||
> M]
|
||||
|
|
|
@ -6,7 +6,3 @@
|
|||
< (--> (in-hole E ((hd @ τ) (((cons @ τ) v_1) v_2)))
|
||||
---
|
||||
> (--> (in-hole E ((hd @ τ) ((cons @ τ) v_1)))
|
||||
261c261
|
||||
< M]
|
||||
---
|
||||
> M]
|
||||
|
|
|
@ -7,7 +7,3 @@
|
|||
< (v E)))
|
||||
---
|
||||
> (E M)))
|
||||
261c260
|
||||
< M]
|
||||
---
|
||||
> M]
|
||||
|
|
|
@ -6,7 +6,3 @@
|
|||
< σ]
|
||||
---
|
||||
> int]
|
||||
261c261
|
||||
< M]
|
||||
---
|
||||
> M]
|
||||
|
|
|
@ -6,7 +6,3 @@
|
|||
< [(lookup (x σ Γ) x)
|
||||
---
|
||||
> [(lookup (x σ Γ) x_2)
|
||||
261c261
|
||||
< M]
|
||||
---
|
||||
> M]
|
||||
|
|
|
@ -291,4 +291,3 @@
|
|||
(begin0
|
||||
(generate-term poly-stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
|
|
|
@ -258,7 +258,7 @@
|
|||
(generate-term poly-stlc #:satisfying
|
||||
(typeof • ((((map @ τ_1) @ τ_2) v) (((cons @ τ_1) v_1) v_2)) τ) 5)])
|
||||
[`(typeof • ,M ,τ)
|
||||
M]
|
||||
M]
|
||||
[#f #f]))
|
||||
(define (typed-generator)
|
||||
(let ([g (redex-generator poly-stlc (typeof • M τ) 5)])
|
||||
|
|
Loading…
Reference in New Issue
Block a user