chore: move more tests to new frontend
This commit is contained in:
parent
a8de3c5115
commit
f242a958fc
6 changed files with 10 additions and 6 deletions
|
|
@ -1,8 +1,8 @@
|
|||
def foo {α} (f : forall {β}, β → β) (a : α) : α :=
|
||||
f a
|
||||
|
||||
new_frontend
|
||||
|
||||
def foo {α} (f : {β : Type _} → β → β) (a : α) : α :=
|
||||
f a
|
||||
|
||||
#check_failure let g := id; foo g true -- fails
|
||||
/-
|
||||
Expands to
|
||||
|
|
|
|||
|
|
@ -1,3 +1,5 @@
|
|||
new_frontend
|
||||
|
||||
axiom f : ∀ (A : Type), A → Type
|
||||
|
||||
def ex5b (α : Type) (a : α) : ∀ (A : Type), A → Type :=
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
import Lean.Parser
|
||||
|
||||
new_frontend
|
||||
def test : IO Unit :=
|
||||
if System.Platform.isWindows then
|
||||
pure () -- TODO investigate why the following doesn't work on Windows
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
new_frontend
|
||||
open Lean
|
||||
|
||||
def f : Name → Name
|
||||
|
|
|
|||
|
|
@ -1,6 +1,5 @@
|
|||
#print Nat
|
||||
|
||||
new_frontend
|
||||
#print Nat
|
||||
|
||||
private def foo (x : Nat) : Nat := x + 1
|
||||
|
||||
|
|
|
|||
|
|
@ -1,3 +1,5 @@
|
|||
new_frontend
|
||||
|
||||
axiom TrustMe {p : Prop} : p
|
||||
|
||||
def x := (1, 2)
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue