diff options
author | Son Ho | 2023-07-04 12:49:37 +0200 |
---|---|---|
committer | Son Ho | 2023-07-04 12:49:37 +0200 |
commit | 4fd17e4bb91eb46d4704643dfbfbbf0874837b07 (patch) | |
tree | 5ebcc4cda3a522e7bad4e475423b87fd83279420 /backends/lean/Base/Diverge/Elab.lean | |
parent | 40e21034fa9e955734351b78a8cc5f16315418bd (diff) |
Make Diverge use Primitives
Diffstat (limited to '')
-rw-r--r-- | backends/lean/Base/Diverge/Elab.lean | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backends/lean/Base/Diverge/Elab.lean b/backends/lean/Base/Diverge/Elab.lean index cc580265..41209021 100644 --- a/backends/lean/Base/Diverge/Elab.lean +++ b/backends/lean/Base/Diverge/Elab.lean @@ -174,7 +174,7 @@ private def list_nth_out_ty_inner (a :Type) (scrut1: @Sigma (List a) (fun (_ls : (fun (_ls : List a) => Int) (fun (_scrut1:@Sigma (List a) (fun (_ls : List a) => Int)) => Type) scrut1 - (fun (_ls : List a) (_i : Int) => Diverge.Primitives.Result a) + (fun (_ls : List a) (_i : Int) => Primitives.Result a) private def list_nth_out_ty_outer (scrut0 : @Sigma (Type) (fun (a:Type) => @Sigma (List a) (fun (_ls : List a) => Int))) := |