fix: bug at toLCNF
This commit is contained in:
parent
c9ccc9c253
commit
e931c6b5b5
2 changed files with 8 additions and 1 deletions
|
|
@ -440,7 +440,7 @@ where
|
|||
visitLet body (xs.push value)
|
||||
else
|
||||
let type' ← liftMetaM <| toLCNFType type
|
||||
let value' ← visitChild value
|
||||
let value' ← visit value
|
||||
let x ← mkLetDecl binderName type value type' value'
|
||||
visitLet body (xs.push x)
|
||||
| _ =>
|
||||
|
|
|
|||
|
|
@ -33,3 +33,10 @@ noncomputable abbrev TupleN : (n : Fin 1) → TupleNTyp n.val
|
|||
|
||||
set_option pp.proofs true
|
||||
#eval Compiler.compile #[``TupleN]
|
||||
|
||||
|
||||
def userControlled (a b : Nat) :=
|
||||
let f := fun _ => a
|
||||
f () + b
|
||||
|
||||
#eval Compiler.compile #[``userControlled]
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue